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
verumproof
let G1,
G2 be
strict AbGroup;
( 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)
;
G1 = G2
hence
G1 = G2
by A8, A10, A12, BINOP_1:2;
verum
end;