let A, B be strict multMagma ; :: thesis: ( ( for x being set holds
( ( x in the carrier of A implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of A ) & ( for f, g being Homeomorphism of T holds the multF of A . f,g = g * f ) ) ) & ( for x being set holds
( ( x in the carrier of B implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of B ) & ( for f, g being Homeomorphism of T holds the multF of B . f,g = g * f ) ) ) implies A = B )
assume that
A5: for x being set holds
( ( x in the carrier of A implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of A ) & ( for f, g being Homeomorphism of T holds the multF of A . f,g = g * f ) ) and
A6: for x being set holds
( ( x in the carrier of B implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of B ) & ( for f, g being Homeomorphism of T holds the multF of B . f,g = g * f ) ) ; :: thesis: A = B
defpred S₁[ set ] means $1 is Homeomorphism of T;
A7: for x being set holds
( x in the carrier of A iff S₁[x] ) by A5;
A8: for x being set holds
( x in the carrier of B iff S₁[x] ) by A6;
A9: the carrier of A = the carrier of B from XBOOLE_0:sch 2(A7, A8);
for c, d being set st c in the carrier of A & d in the carrier of A holds
the multF of A . c,d = the multF of B . c,d

proof

let c, d be set ; :: thesis: ( c in the carrier of A & d in the carrier of A implies the multF of A . c,d = the multF of B . c,d )
assume ( c in the carrier of A & d in the carrier of A ) ; :: thesis: the multF of A . c,d = the multF of B . c,d
then reconsider f = c, g = d as Homeomorphism of T by A5;
thus the multF of A . c,d = g * f by A5
.= the multF of B . c,d by A6 ; :: thesis: verum

end;

hence A = B by A9, BINOP_1:1; :: thesis: verum