thus
for G1, G2 being strict AbGroup st the carrier of G1 = n -Matrices_over F & ( for A, B being Matrix of n,F holds the addF of G1 . (A,B) = A + B ) & 0. G1 = 0. (F,n) & the carrier of G2 = n -Matrices_over F & ( for A, B being Matrix of n,F holds the addF of G2 . (A,B) = A + B ) & 0. G2 = 0. (F,n) holds

G1 = G2 :: thesis: verum

G1 = G2 :: thesis: verum

proof

let G1, G2 be strict AbGroup; :: thesis: ( the carrier of G1 = n -Matrices_over F & ( for A, B being Matrix of n,F holds the addF of G1 . (A,B) = A + B ) & 0. G1 = 0. (F,n) & the carrier of G2 = n -Matrices_over F & ( for A, B being Matrix of n,F holds the addF of G2 . (A,B) = A + B ) & 0. G2 = 0. (F,n) implies G1 = G2 )

assume that

A8: the carrier of G1 = n -Matrices_over F and

A9: for A, B being Matrix of n,F holds the addF of G1 . (A,B) = A + B and

A10: ( 0. G1 = 0. (F,n) & the carrier of G2 = n -Matrices_over F ) and

A11: for A, B being Matrix of n,F holds the addF of G2 . (A,B) = A + B and

A12: 0. G2 = 0. (F,n) ; :: thesis: G1 = G2

end;assume that

A8: the carrier of G1 = n -Matrices_over F and

A9: for A, B being Matrix of n,F holds the addF of G1 . (A,B) = A + B and

A10: ( 0. G1 = 0. (F,n) & the carrier of G2 = n -Matrices_over F ) and

A11: for A, B being Matrix of n,F holds the addF of G2 . (A,B) = A + B and

A12: 0. G2 = 0. (F,n) ; :: thesis: G1 = G2

now :: thesis: for a, b being Element of G1 holds the addF of G1 . (a,b) = the addF of G2 . (a,b)

hence
G1 = G2
by A8, A10, A12, BINOP_1:2; :: thesis: verumlet a, b be Element of G1; :: thesis: the addF of G1 . (a,b) = the addF of G2 . (a,b)

reconsider A = a, B = b as Matrix of n,F by A8, Th2;

thus the addF of G1 . (a,b) = A + B by A9

.= the addF of G2 . (a,b) by A11 ; :: thesis: verum

end;reconsider A = a, B = b as Matrix of n,F by A8, Th2;

thus the addF of G1 . (a,b) = A + B by A9

.= the addF of G2 . (a,b) by A11 ; :: thesis: verum