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 A = a as Matrix of n,F by Th31;
reconsider B = b as Matrix of n,F by Th31;
reconsider c = A + B as Element of n -Matrices_over F by Th31;
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);
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 Th31;
then ex A', B' being Matrix of n,F st
( A = A' & B = B' & h . A,B = A' + B' ) 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 Th31;
reconsider b = - A as Element of n -Matrices_over F by Th31;
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;

reconsider A0 = 0. F,n as Element of n -Matrices_over F ;
set G = addLoopStr(# (n -Matrices_over F),h,A0 #);
( 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 5 :: thesis: a + b = b + a
reconsider A = a, B = b as Matrix of n,F by Th31;
thus a + b = A + B by A3
.= B + A by Th32
.= b + a by A3 ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 6 :: 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 Th31;
thus (a + b) + c = h . (A + B),C by A3
.= (A + B) + C by A3
.= A + (B + C) by Th33
.= h . A,(B + C) by A3
.= a + (b + c) by A3 ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 7 :: 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 Th31;
thus a + (0. addLoopStr(# (n -Matrices_over F),h,A0 #)) = A + (0. F,n) by A3
.= a by Th34 ; :: 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 & b = - A ) by A5;
reconsider b = - A as Element of addLoopStr(# (n -Matrices_over F),h,A0 #) by A6;
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 Th35 ; :: 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