deffunc H₁( set ) -> Subset of S = SigFoaxTau g,f,(CastBool $1,S),R,BASSIGN;
A1: for H being set st H in bool S holds
H₁(H) in bool S ;
consider IT being Function of (bool S),(bool S) such that
A2: for H being set st H in bool S holds
IT . H = H₁(H) from FUNCT_2:sch 2(A1);
A3: for H being Subset of S holds IT . H = SigFoaxTau g,f,H,R,BASSIGN

proof

let H be Subset of S; :: thesis: IT . H = SigFoaxTau g,f,H,R,BASSIGN
CastBool H,S = H by Def5;
hence IT . H = SigFoaxTau g,f,H,R,BASSIGN by A2; :: thesis: verum

end;

for H1, H2 being Subset of S st H1 c= H2 holds
IT . H1 c= IT . H2

proof

let H1, H2 be Subset of S; :: thesis: ( H1 c= H2 implies IT . H1 c= IT . H2 )
assume A4: H1 c= H2 ; :: thesis: IT . H1 c= IT . H2
A5: IT . H2 = SigFoaxTau g,f,H2,R,BASSIGN by A3;
IT . H1 = SigFoaxTau g,f,H1,R,BASSIGN by A3;
hence IT . H1 c= IT . H2 by A4, A5, Th45; :: thesis: verum

end;

then reconsider IT = IT as V224() Function of (bool S),(bool S) by KNASTER:def 3;
take IT ; :: thesis: for H being Subset of S holds IT . H = SigFoaxTau g,f,H,R,BASSIGN
thus for H being Subset of S holds IT . H = SigFoaxTau g,f,H,R,BASSIGN by A3; :: thesis: verum