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

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

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

let 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;

hence G1 = G2 by A8, A10, A12, BINOP_1:2; :: thesis: verum

end;