defpred S1[ object ] means $1 is Homeomorphism of T;
consider A being set such that
A1:
for q being object holds
( q in A iff ( q in Funcs ( the carrier of T, the carrier of T) & S1[q] ) )
from XBOOLE_0:sch 1();
A2:
for f being Homeomorphism of T holds f in A
by A1, FUNCT_2:9;
then reconsider A = A as non empty set ;
defpred S2[ Element of A, Element of A, Element of A] means ex f, g being Homeomorphism of T st
( $1 = f & $2 = g & $3 = g * f );
A3:
for x, y being Element of A ex z being Element of A st S2[x,y,z]
consider o being BinOp of A such that
A4:
for a, b being Element of A holds S2[a,b,o . (a,b)]
from BINOP_1:sch 3(A3);
take G = multMagma(# A,o #); for x being set holds
( ( x in the carrier of G implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of G ) & ( for f, g being Homeomorphism of T holds the multF of G . (f,g) = g * f ) )
let x be set ; ( ( x in the carrier of G implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of G ) & ( for f, g being Homeomorphism of T holds the multF of G . (f,g) = g * f ) )
thus
( x in the carrier of G iff x is Homeomorphism of T )
by A1, A2; for f, g being Homeomorphism of T holds the multF of G . (f,g) = g * f
let f, g be Homeomorphism of T; the multF of G . (f,g) = g * f
reconsider f1 = f, g1 = g as Element of A by A2;
ex m, n being Homeomorphism of T st
( f1 = m & g1 = n & o . (f1,g1) = n * m )
by A4;
hence
the multF of G . (f,g) = g * f
; verum