deffunc H1( Subset of (Funcs (F1(),F1()))) -> Subset of (Funcs (F1(),F1())) = MltClos1 (F2(),$1);
consider phi being Function of (bool (Funcs (F1(),F1()))),(bool (Funcs (F1(),F1()))) such that
A5: for X being Subset of (Funcs (F1(),F1())) holds phi . X = H1(X) from FUNCT_2:sch 4();
 set SP = { f where f is Function of F1(),F1() : P1[f] } ;
{ f where f is Function of F1(),F1() : P1[f] } c= Funcs (F1(),F1())
proof
let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in { f where f is Function of F1(),F1() : P1[f] } or f in Funcs (F1(),F1()) )
assume f in { f where f is Function of F1(),F1() : P1[f] } ; :: thesis: f in Funcs (F1(),F1())
then ex g being Function of F1(),F1() st
( f = g & P1[g] ) ;
hence f in Funcs (F1(),F1()) by FUNCT_2:9; :: thesis: verum
end;
then reconsider SP = { f where f is Function of F1(),F1() : P1[f] } as Subset of (Funcs (F1(),F1())) ;
phi . SP c= SP
proof
let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in phi . SP or f in SP )
assume f in phi . SP ; :: thesis: f in SP
then f in MltClos1 (F2(),SP) by A5;
per cases then ( ex u being Element of F1() st
( u in F2() & f = (curry' the multF of F1()) . u ) or ex u being Element of F1() st
( u in F2() & f = (curry the multF of F1()) . u ) or ex g, h being Permutation of F1() st
( g in SP & h in SP & f = g * h ) or ex g being Permutation of F1() st
( g in SP & f = g " ) ) by Def37;
suppose ex u being Element of F1() st
( u in F2() & f = (curry' the multF of F1()) . u ) ; :: thesis: f in SP
then consider u being Element of F1() such that
A6: ( u in F2() & f = (curry' the multF of F1()) . u ) ;
reconsider f = f as Function of F1(),F1() by A6;
for x being Element of F1() holds f . x = x * u by A6, FUNCT_5:70;
then P1[f] by A1, A6;
hence f in SP ; :: thesis: verum
end;
suppose ex u being Element of F1() st
( u in F2() & f = (curry the multF of F1()) . u ) ; :: thesis: f in SP
then consider u being Element of F1() such that
A7: ( u in F2() & f = (curry the multF of F1()) . u ) ;
reconsider f = f as Function of F1(),F1() by A7;
for x being Element of F1() holds f . x = u * x by A7, FUNCT_5:69;
then P1[f] by A2, A7;
hence f in SP ; :: thesis: verum
end;
suppose ex g, h being Permutation of F1() st
( g in SP & h in SP & f = g * h ) ; :: thesis: f in SP
then consider g, h being Permutation of F1() such that
A8: ( g in SP & h in SP & f = g * h ) ;
consider g2 being Function of F1(),F1() such that
A9: ( g = g2 & P1[g2] ) by A8;
A10: ex h2 being Function of F1(),F1() st
( h = h2 & P1[h2] ) by A8;
P1[g * h] by A10, A3, A9;
hence f in SP by A8; :: thesis: verum
end;
suppose ex g being Permutation of F1() st
( g in SP & f = g " ) ; :: thesis: f in SP
then consider g being Permutation of F1() such that
A11: ( g in SP & f = g " ) ;
ex g2 being Function of F1(),F1() st
( g = g2 & P1[g2] ) by A11;
then P1[g " ] by A4;
hence f in SP by A11; :: thesis: verum
end;
end;
end;
then A12: Mlt F2() c= SP by Th34, A5;
let f be Function of F1(),F1(); :: thesis: ( f in Mlt F2() implies P1[f] )
assume f in Mlt F2() ; :: thesis: P1[f]
then f in SP by A12;
then ex g being Function of F1(),F1() st
( f = g & P1[g] ) ;
hence P1[f] ; :: thesis: verum