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

proof

let G be Subset of S; :: thesis: IT . G = SigFaxTau f,G,R,BASSIGN
H₁(G) = SigFaxTau f,G,R,BASSIGN by Def5;
hence IT . G = SigFaxTau f,G,R,BASSIGN by A2; :: thesis: verum

end;

for G1, G2 being Subset of S st G1 c= G2 holds
IT . G1 c= IT . G2

proof

let G1, G2 be Subset of S; :: thesis: ( G1 c= G2 implies IT . G1 c= IT . G2 )
assume A4: G1 c= G2 ; :: thesis: IT . G1 c= IT . G2
A5: IT . G2 = SigFaxTau f,G2,R,BASSIGN by A3;
IT . G1 = SigFaxTau f,G1,R,BASSIGN by A3;
hence IT . G1 c= IT . G2 by A4, A5, Th37; :: thesis: verum

end;

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