defpred S₁[ 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) & S₁[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) & S₁[x,y] ) )
assume x in Union the Sorts of (Free (S,X)) ; :: thesis: ex y being object st
( y in bool (X . s) & S₁[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) & S₁[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
S₁[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