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
A7: the carrier of G1 = n -Matrices_over F and
A8: for A, B being Matrix of n,F holds the addF of G1 . A,B = A + B and
A9: 0. G1 = 0. F,n and
A10: 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

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 A7, Th31;
thus the addF of G1 . a,b = A + B by A8
.= the addF of G2 . a,b by A11 ; :: thesis: verum

end;

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

end;