reconsider A0 = 0. (F,n) as Element of n -Matrices_over F ;
defpred S₁[ Element of n -Matrices_over F, Element of n -Matrices_over F, Element of n -Matrices_over F] means ex A, B being Matrix of n,F st
( $1 = A & $2 = B & $3 = A + B );
A1: for a, b being Element of n -Matrices_over F ex c being Element of n -Matrices_over F st S₁[a,b,c]

proof

let a, b be Element of n -Matrices_over F; :: thesis: ex c being Element of n -Matrices_over F st S₁[a,b,c]
reconsider B = b as Matrix of n,F by Th2;
reconsider A = a as Matrix of n,F by Th2;
reconsider c = A + B as Element of n -Matrices_over F by Th2;
take c ; :: thesis: S₁[a,b,c]
thus S₁[a,b,c] ; :: thesis: verum

end;

consider h being BinOp of (n -Matrices_over F) such that
A2: for a, b being Element of n -Matrices_over F holds S₁[a,b,h . (a,b)] from BINOP_1:sch 3(A1);
set G = addLoopStr(# (n -Matrices_over F),h,A0 #);
A3: for A, B being Matrix of n,F holds h . (A,B) = A + B

proof

let A, B be Matrix of n,F; :: thesis: h . (A,B) = A + B
( A is Element of n -Matrices_over F & B is Element of n -Matrices_over F ) by Th2;
then ex A9, B9 being Matrix of n,F st
( A = A9 & B = B9 & h . (A,B) = A9 + B9 ) by A2;
hence h . (A,B) = A + B ; :: thesis: verum

end;

A4: for a being Element of n -Matrices_over F ex b being Element of n -Matrices_over F ex A being Matrix of n,F st
( a = A & b = - A )

proof

let a be Element of n -Matrices_over F; :: thesis: ex b being Element of n -Matrices_over F ex A being Matrix of n,F st
( a = A & b = - A )
reconsider A = a as Matrix of n,F by Th2;
reconsider b = - A as Element of n -Matrices_over F by Th2;
take b ; :: thesis: ex A being Matrix of n,F st
( a = A & b = - A )
thus ex A being Matrix of n,F st
( a = A & b = - A ) ; :: thesis: verum

end;

( addLoopStr(# (n -Matrices_over F),h,A0 #) is Abelian & addLoopStr(# (n -Matrices_over F),h,A0 #) is add-associative & addLoopStr(# (n -Matrices_over F),h,A0 #) is right_zeroed & addLoopStr(# (n -Matrices_over F),h,A0 #) is right_complementable )

proof

thus addLoopStr(# (n -Matrices_over F),h,A0 #) is Abelian :: thesis: ( addLoopStr(# (n -Matrices_over F),h,A0 #) is add-associative & addLoopStr(# (n -Matrices_over F),h,A0 #) is right_zeroed & addLoopStr(# (n -Matrices_over F),h,A0 #) is right_complementable )

proof

let a, b be Element of addLoopStr(# (n -Matrices_over F),h,A0 #); :: according to RLVECT_1:def 2 :: thesis: a + b = b + a
reconsider A = a, B = b as Matrix of n,F by Th2;
thus a + b = A + B by A3
.= B + A by Th3
.= b + a by A3 ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 3 :: thesis: ( addLoopStr(# (n -Matrices_over F),h,A0 #) is right_zeroed & addLoopStr(# (n -Matrices_over F),h,A0 #) is right_complementable )

let a, b, c be Element of addLoopStr(# (n -Matrices_over F),h,A0 #); :: thesis: (a + b) + c = a + (b + c)
reconsider A = a, B = b, C = c as Matrix of n,F by Th2;
thus (a + b) + c = h . ((A + B),C) by A3
.= (A + B) + C by A3
.= A + (B + C) by Th4
.= h . (A,(B + C)) by A3
.= a + (b + c) by A3 ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 4 :: thesis: addLoopStr(# (n -Matrices_over F),h,A0 #) is right_complementable

let a be Element of addLoopStr(# (n -Matrices_over F),h,A0 #); :: thesis: a + (0. addLoopStr(# (n -Matrices_over F),h,A0 #)) = a
reconsider A = a as Matrix of n,F by Th2;
thus a + (0. addLoopStr(# (n -Matrices_over F),h,A0 #)) = A + (0. (F,n)) by A3
.= a by Th5 ; :: thesis: verum

end;

let a be Element of addLoopStr(# (n -Matrices_over F),h,A0 #); :: according to ALGSTR_0:def 16 :: thesis: a is right_complementable
consider b being Element of n -Matrices_over F such that
A5: ex A being Matrix of n,F st
( a = A & b = - A ) by A4;
consider A being Matrix of n,F such that
A6: a = A and
A7: b = - A by A5;
reconsider b = - A as Element of addLoopStr(# (n -Matrices_over F),h,A0 #) by A7;
take b ; :: according to ALGSTR_0:def 11 :: thesis: a + b = 0. addLoopStr(# (n -Matrices_over F),h,A0 #)
thus a + b = A + (- A) by A3, A6
.= 0. addLoopStr(# (n -Matrices_over F),h,A0 #) by Th6 ; :: thesis: verum

end;

then reconsider G = addLoopStr(# (n -Matrices_over F),h,A0 #) as strict AbGroup ;
take G ; :: thesis: ( the carrier of G = n -Matrices_over F & ( for A, B being Matrix of n,F holds the addF of G . (A,B) = A + B ) & 0. G = 0. (F,n) )
thus ( the carrier of G = n -Matrices_over F & ( for A, B being Matrix of n,F holds the addF of G . (A,B) = A + B ) & 0. G = 0. (F,n) ) by A3; :: thesis: verum