reconsider A0 = 0. (F,n) as Element of n -Matrices_over F ;

defpred S_{1}[ 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_{1}[a,b,c]

A2: for a, b being Element of n -Matrices_over F holds S_{1}[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

( a = A & b = - A )

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

defpred S

( $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

proof

consider h being BinOp of (n -Matrices_over F) such that
let a, b be Element of n -Matrices_over F; :: thesis: ex c being Element of n -Matrices_over F st S_{1}[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_{1}[a,b,c]

thus S_{1}[a,b,c]
; :: thesis: verum

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

thus S

A2: for a, b being Element of n -Matrices_over F holds S

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

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

( a = A & b = - A )

proof

( 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 )
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;( 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

proof

then reconsider G = addLoopStr(# (n -Matrices_over F),h,A0 #) as strict AbGroup ;
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 )

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

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

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 #); :: according to ALGSTR_0:def 16 :: thesis: a 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;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

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

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