let F1, F2 be FUNCTION_DOMAIN of the carrier of G, the carrier of G; :: thesis: ( ( for f being Element of Funcs ( the carrier of G, the carrier of G) holds

( f in F1 iff ex a being Element of G st

for x being Element of G holds f . x = x |^ a ) ) & ( for f being Element of Funcs ( the carrier of G, the carrier of G) holds

( f in F2 iff ex a being Element of G st

for x being Element of G holds f . x = x |^ a ) ) implies F1 = F2 )

assume that

A4: for f being Element of Funcs ( the carrier of G, the carrier of G) holds

( f in F1 iff ex a being Element of G st

for x being Element of G holds f . x = x |^ a ) and

A5: for f being Element of Funcs ( the carrier of G, the carrier of G) holds

( f in F2 iff ex a being Element of G st

for x being Element of G holds f . x = x |^ a ) ; :: thesis: F1 = F2

A6: F2 c= F1

( f in F1 iff ex a being Element of G st

for x being Element of G holds f . x = x |^ a ) ) & ( for f being Element of Funcs ( the carrier of G, the carrier of G) holds

( f in F2 iff ex a being Element of G st

for x being Element of G holds f . x = x |^ a ) ) implies F1 = F2 )

assume that

A4: for f being Element of Funcs ( the carrier of G, the carrier of G) holds

( f in F1 iff ex a being Element of G st

for x being Element of G holds f . x = x |^ a ) and

A5: for f being Element of Funcs ( the carrier of G, the carrier of G) holds

( f in F2 iff ex a being Element of G st

for x being Element of G holds f . x = x |^ a ) ; :: thesis: F1 = F2

A6: F2 c= F1

proof

F1 c= F2
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in F2 or q in F1 )

assume A7: q in F2 ; :: thesis: q in F1

then q is Function of the carrier of G, the carrier of G by FUNCT_2:def 12;

then reconsider b1 = q as Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:9;

ex a being Element of G st

for x being Element of G holds b1 . x = x |^ a by A5, A7;

hence q in F1 by A4; :: thesis: verum

end;assume A7: q in F2 ; :: thesis: q in F1

then q is Function of the carrier of G, the carrier of G by FUNCT_2:def 12;

then reconsider b1 = q as Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:9;

ex a being Element of G st

for x being Element of G holds b1 . x = x |^ a by A5, A7;

hence q in F1 by A4; :: thesis: verum

proof

hence
F1 = F2
by A6, XBOOLE_0:def 10; :: thesis: verum
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in F1 or q in F2 )

assume A8: q in F1 ; :: thesis: q in F2

then q is Function of the carrier of G, the carrier of G by FUNCT_2:def 12;

then reconsider b1 = q as Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:9;

ex a being Element of G st

for x being Element of G holds b1 . x = x |^ a by A4, A8;

hence q in F2 by A5; :: thesis: verum

end;assume A8: q in F1 ; :: thesis: q in F2

then q is Function of the carrier of G, the carrier of G by FUNCT_2:def 12;

then reconsider b1 = q as Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:9;

ex a being Element of G st

for x being Element of G holds b1 . x = x |^ a by A4, A8;

hence q in F2 by A5; :: thesis: verum