defpred S₁[ object ] means $1 is Homeomorphism of T;
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
A7: for x being object holds
( x in the carrier of B iff S₁[x] ) by A6;
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;

A9: for x being object holds
( x in the carrier of A iff S₁[x] ) by A5;
the carrier of A = the carrier of B from XBOOLE_0:sch 2(A9, A7);
hence A = B by A8, BINOP_1:1; :: thesis: verum