defpred S1[ object , object ] means ex t being Element of (Free (S,X)) st
( t = $1 & $2 = (S variables_in t) . s );
A3: now :: thesis: for x being object st x in Union the Sorts of (Free (S,X)) holds
ex y being object st
( y in bool (X . s) & S1[x,y] )
let x be object ; :: thesis: ( x in Union the Sorts of (Free (S,X)) implies ex y being object st
( y in bool (X . s) & S1[x,y] ) )
assume x in Union the Sorts of (Free (S,X)) ; :: thesis: ex y being object st
( y in bool (X . s) & S1[x,y] )
then reconsider t = x as Element of (Free (S,X)) ;
S variables_in t c= X by MSAFREE3:27;
then (S variables_in t) . s c= X . s ;
hence ex y being object st
( y in bool (X . s) & S1[x,y] ) ; :: thesis: verum
end;
consider f being Function such that
A4: ( dom f = Union the Sorts of (Free (S,X)) & rng f c= bool (X . s) ) and
A5: for x being object st x in Union the Sorts of (Free (S,X)) holds
S1[x,f . x] from FUNCT_1:sch 6(A3);
 reconsider f = f as Function of (Union the Sorts of (Free (S,X))),(bool (X . s)) by A4, FUNCT_2:2;
take f ; :: thesis: for t being Element of (Free (S,X)) holds f . t = (S variables_in t) . s
let x be Element of (Free (S,X)); :: thesis: f . x = (S variables_in x) . s
ex t being Element of (Free (S,X)) st
( t = x & f . x = (S variables_in t) . s ) by A5;
hence f . x = (S variables_in x) . s ; :: thesis: verum