let S1, S2 be Subset of (Funcs (Q,Q)); :: thesis: ( ( for f being object holds
( f in S1 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 " ) ) ) ) & ( for f being object holds
( f in S2 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 " ) ) ) ) implies S1 = S2 )
assume that
A4: for f being object holds
( f in S1 iff S2[Q,H,S,f] ) and
A5: for f being object holds
( f in S2 iff S2[Q,H,S,f] ) ; :: thesis: S1 = S2
now :: thesis: for f being Element of Funcs (Q,Q) holds
( f in S1 iff f in S2 )
let f be Element of Funcs (Q,Q); :: thesis: ( f in S1 iff f in S2 )
( f in S1 iff S2[Q,H,S,f] ) by A4;
hence ( f in S1 iff f in S2 ) by A5; :: thesis: verum
end;
hence S1 = S2 by SUBSET_1:3; :: thesis: verum