defpred S₁[ set , set ] means ex t being Element of (Free S,X) st
( t = $1 & $2 = (S variables_in t) . s );

A3: now

let x be set ; :: thesis: ( x in Union the Sorts of (Free S,X) implies ex y being set st
( y in bool (X . s) & S₁[x,y] ) )
assume x in Union the Sorts of (Free S,X) ; :: thesis: ex y being set 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:28;
then (S variables_in t) . s c= X . s by PBOOLE:def 5;
hence ex y being set 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 set st x in Union the Sorts of (Free S,X) holds
S₁[x,f . x] from WELLORD2:sch 1(A3);
reconsider f = f as Function of (Union the Sorts of (Free S,X)),(bool (X . s)) by A4, FUNCT_2:4;
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