set mQ = the multF of Q;
set LH = { ((curry' the multF of Q) . u) where u is Element of Q : u in H } ;
set RH = { ((curry the multF of Q) . u) where u is Element of Q : u in H } ;
set SC = { (g * h) where g, h is Permutation of Q : ( g in S & h in S ) } ;
set SI = { (g ") where g is Permutation of Q : g in S } ;
set Y = (( { ((curry' the multF of Q) . u) where u is Element of Q : u in H } \/ { ((curry the multF of Q) . u) where u is Element of Q : u in H } ) \/ { (g * h) where g, h is Permutation of Q : ( g in S & h in S ) } ) \/ { (g ") where g is Permutation of Q : g in S } ;
A1: { ((curry' the multF of Q) . u) where u is Element of Q : u in H } c= Funcs (Q,Q)

proof

let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in { ((curry' the multF of Q) . u) where u is Element of Q : u in H } or f in Funcs (Q,Q) )
assume f in { ((curry' the multF of Q) . u) where u is Element of Q : u in H } ; :: thesis: f in Funcs (Q,Q)
then ex u being Element of Q st
( f = (curry' the multF of Q) . u & u in H ) ;
hence f in Funcs (Q,Q) ; :: thesis: verum

end;

{ ((curry the multF of Q) . u) where u is Element of Q : u in H } c= Funcs (Q,Q)

proof

let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in { ((curry the multF of Q) . u) where u is Element of Q : u in H } or f in Funcs (Q,Q) )
assume f in { ((curry the multF of Q) . u) where u is Element of Q : u in H } ; :: thesis: f in Funcs (Q,Q)
then ex u being Element of Q st
( f = (curry the multF of Q) . u & u in H ) ;
hence f in Funcs (Q,Q) ; :: thesis: verum

end;

then A2: { ((curry' the multF of Q) . u) where u is Element of Q : u in H } \/ { ((curry the multF of Q) . u) where u is Element of Q : u in H } is Subset of (Funcs (Q,Q)) by A1, XBOOLE_1:8;
{ (g * h) where g, h is Permutation of Q : ( g in S & h in S ) } c= Funcs (Q,Q)

proof

let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in { (g * h) where g, h is Permutation of Q : ( g in S & h in S ) } or f in Funcs (Q,Q) )
assume f in { (g * h) where g, h is Permutation of Q : ( g in S & h in S ) } ; :: thesis: f in Funcs (Q,Q)
then ex g, h being Permutation of Q st
( f = g * h & g in S & h in S ) ;
hence f in Funcs (Q,Q) by FUNCT_2:9; :: thesis: verum

end;

then A3: ( { ((curry' the multF of Q) . u) where u is Element of Q : u in H } \/ { ((curry the multF of Q) . u) where u is Element of Q : u in H } ) \/ { (g * h) where g, h is Permutation of Q : ( g in S & h in S ) } is Subset of (Funcs (Q,Q)) by A2, XBOOLE_1:8;
{ (g ") where g is Permutation of Q : g in S } c= Funcs (Q,Q)

proof

let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in { (g ") where g is Permutation of Q : g in S } or f in Funcs (Q,Q) )
assume f in { (g ") where g is Permutation of Q : g in S } ; :: thesis: f in Funcs (Q,Q)
then ex g being Permutation of Q st
( f = g " & g in S ) ;
hence f in Funcs (Q,Q) by FUNCT_2:9; :: thesis: verum

end;

then reconsider Y = (( { ((curry' the multF of Q) . u) where u is Element of Q : u in H } \/ { ((curry the multF of Q) . u) where u is Element of Q : u in H } ) \/ { (g * h) where g, h is Permutation of Q : ( g in S & h in S ) } ) \/ { (g ") where g is Permutation of Q : g in S } as Subset of (Funcs (Q,Q)) by A3, XBOOLE_1:8;
take Y ; :: thesis: for f being object holds
( f in Y iff ( ex u being Element of Q st
( u in H & f = (curry' the multF of Q) . u ) or ex u being Element of Q st
( u in H & f = (curry the multF of Q) . u ) or ex g, h being Permutation of Q st
( g in S & h in S & f = g * h ) or ex g being Permutation of Q st
( g in S & f = g " ) ) )
let f be object ; :: thesis: ( f in Y iff ( ex u being Element of Q st
( u in H & f = (curry' the multF of Q) . u ) or ex u being Element of Q st
( u in H & f = (curry the multF of Q) . u ) or ex g, h being Permutation of Q st
( g in S & h in S & f = g * h ) or ex g being Permutation of Q st
( g in S & f = g " ) ) )
thus ( f in Y implies S₂[Q,H,S,f] ) :: thesis: ( ( ex u being Element of Q st
( u in H & f = (curry' the multF of Q) . u ) or ex u being Element of Q st
( u in H & f = (curry the multF of Q) . u ) or ex g, h being Permutation of Q st
( g in S & h in S & f = g * h ) or ex g being Permutation of Q st
( g in S & f = g " ) ) implies f in Y )

proof

assume f in Y ; :: thesis: S₂[Q,H,S,f]
then ( f in ( { ((curry' the multF of Q) . u) where u is Element of Q : u in H } \/ { ((curry the multF of Q) . u) where u is Element of Q : u in H } ) \/ { (g * h) where g, h is Permutation of Q : ( g in S & h in S ) } or f in { (g ") where g is Permutation of Q : g in S } ) by XBOOLE_0:def 3;
then ( f in { ((curry' the multF of Q) . u) where u is Element of Q : u in H } \/ { ((curry the multF of Q) . u) where u is Element of Q : u in H } or f in { (g * h) where g, h is Permutation of Q : ( g in S & h in S ) } or f in { (g ") where g is Permutation of Q : g in S } ) by XBOOLE_0:def 3;

per cases then ( f in { ((curry' the multF of Q) . u) where u is Element of Q : u in H } or f in { ((curry the multF of Q) . u) where u is Element of Q : u in H } or f in { (g * h) where g, h is Permutation of Q : ( g in S & h in S ) } or f in { (g ") where g is Permutation of Q : g in S } ) by XBOOLE_0:def 3;

suppose f in { ((curry' the multF of Q) . u) where u is Element of Q : u in H } ; :: thesis: S₂[Q,H,S,f]

then ex u being Element of Q st
( f = (curry' the multF of Q) . u & u in H ) ;
hence S₂[Q,H,S,f] ; :: thesis: verum

end;

suppose f in { ((curry the multF of Q) . u) where u is Element of Q : u in H } ; :: thesis: S₂[Q,H,S,f]

then ex u being Element of Q st
( f = (curry the multF of Q) . u & u in H ) ;
hence S₂[Q,H,S,f] ; :: thesis: verum

end;

suppose f in { (g * h) where g, h is Permutation of Q : ( g in S & h in S ) } ; :: thesis: S₂[Q,H,S,f]

then ex g, h being Permutation of Q st
( f = g * h & g in S & h in S ) ;
hence S₂[Q,H,S,f] ; :: thesis: verum

end;

suppose f in { (g ") where g is Permutation of Q : g in S } ; :: thesis: S₂[Q,H,S,f]

then ex g being Permutation of Q st
( f = g " & g in S ) ;
hence S₂[Q,H,S,f] ; :: thesis: verum

end;

end;

end;

assume S₂[Q,H,S,f] ; :: thesis: f in Y
then ( f in { ((curry' the multF of Q) . u) where u is Element of Q : u in H } or f in { ((curry the multF of Q) . u) where u is Element of Q : u in H } or f in { (g * h) where g, h is Permutation of Q : ( g in S & h in S ) } or f in { (g ") where g is Permutation of Q : g in S } ) ;
then ( f in { ((curry' the multF of Q) . u) where u is Element of Q : u in H } \/ { ((curry the multF of Q) . u) where u is Element of Q : u in H } or f in { (g * h) where g, h is Permutation of Q : ( g in S & h in S ) } or f in { (g ") where g is Permutation of Q : g in S } ) by XBOOLE_0:def 3;
then ( f in ( { ((curry' the multF of Q) . u) where u is Element of Q : u in H } \/ { ((curry the multF of Q) . u) where u is Element of Q : u in H } ) \/ { (g * h) where g, h is Permutation of Q : ( g in S & h in S ) } or f in { (g ") where g is Permutation of Q : g in S } ) by XBOOLE_0:def 3;
hence f in Y by XBOOLE_0:def 3; :: thesis: verum