deffunc H_{1}( addLoopStr ) -> Element of the carrier of G = the ZeroF of G;

reconsider GS = RLSStruct(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):] #) as non empty RLSStruct ;

deffunc H_{2}( 1-sorted ) -> set = the carrier of G;

deffunc H_{3}( addLoopStr ) -> Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:] = the addF of G;

A5: GS is right_complementable

hence ( product G is Abelian & product G is add-associative & product G is right_zeroed & product G is right_complementable & product G is vector-distributive & product G is scalar-distributive & product G is scalar-associative & product G is scalar-unital ) by A2, A4, A5, Lm1, Lm2, Lm5; :: thesis: verum

reconsider GS = RLSStruct(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):] #) as non empty RLSStruct ;

deffunc H

deffunc H

A1: now :: thesis: for i being Element of dom (carr G) holds (carr G) . i = H_{2}(G . i)

let i be Element of dom (carr G); :: thesis: (carr G) . i = H_{2}(G . i)

dom G = Seg (len G) by FINSEQ_1:def 3

.= Seg (len (carr G)) by Def4

.= dom (carr G) by FINSEQ_1:def 3 ;

hence (carr G) . i = H_{2}(G . i)
by Def4; :: thesis: verum

end;dom G = Seg (len G) by FINSEQ_1:def 3

.= Seg (len (carr G)) by Def4

.= dom (carr G) by FINSEQ_1:def 3 ;

hence (carr G) . i = H

now :: thesis: for i being Element of dom (carr G) holds (addop G) . i is associative

then A2:
[:(addop G):] is associative
by PRVECT_1:18;let i be Element of dom (carr G); :: thesis: (addop G) . i is associative

( (addop G) . i = H_{3}(G . i) & (carr G) . i = H_{2}(G . i) )
by A1, Def5;

hence (addop G) . i is associative by FVSUM_1:2; :: thesis: verum

end;( (addop G) . i = H

hence (addop G) . i is associative by FVSUM_1:2; :: thesis: verum

now :: thesis: for i being Element of dom (carr G) holds (zeros G) . i is_a_unity_wrt (addop G) . i

then A4:
zeros G is_a_unity_wrt [:(addop G):]
by PRVECT_1:19;let i be Element of dom (carr G); :: thesis: (zeros G) . i is_a_unity_wrt (addop G) . i

A3: (zeros G) . i = 0. (G . i) by Def7;

( (addop G) . i = H_{3}(G . i) & (carr G) . i = H_{2}(G . i) )
by A1, Def5;

hence (zeros G) . i is_a_unity_wrt (addop G) . i by A3, PRVECT_1:1; :: thesis: verum

end;A3: (zeros G) . i = 0. (G . i) by Def7;

( (addop G) . i = H

hence (zeros G) . i is_a_unity_wrt (addop G) . i by A3, PRVECT_1:1; :: thesis: verum

A5: GS is right_complementable

proof

let x be Element of GS; :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable

reconsider y = (Frege (complop G)) . x as Element of GS by FUNCT_2:5;

take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. GS

then [:(addop G):] . (x,y) = the_unity_wrt [:(addop G):] by FINSEQOP:def 1;

hence x + y = 0. GS by A4, BINOP_1:def 8; :: thesis: verum

end;reconsider y = (Frege (complop G)) . x as Element of GS by FUNCT_2:5;

take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. GS

now :: thesis: for i being Element of dom (carr G) holds

( (complop G) . i is_an_inverseOp_wrt (addop G) . i & (addop G) . i is having_a_unity )

then
Frege (complop G) is_an_inverseOp_wrt [:(addop G):]
by PRVECT_1:20;( (complop G) . i is_an_inverseOp_wrt (addop G) . i & (addop G) . i is having_a_unity )

let i be Element of dom (carr G); :: thesis: ( (complop G) . i is_an_inverseOp_wrt (addop G) . i & (addop G) . i is having_a_unity )

0. (G . i) = H_{1}(G . i)
;

then A6: H_{1}(G . i) is_a_unity_wrt H_{3}(G . i)
by PRVECT_1:1;

A7: (complop G) . i = comp (G . i) by Def6;

( (carr G) . i = H_{2}(G . i) & (addop G) . i = H_{3}(G . i) )
by A1, Def5;

hence ( (complop G) . i is_an_inverseOp_wrt (addop G) . i & (addop G) . i is having_a_unity ) by A6, A7, PRVECT_1:2, SETWISEO:def 2; :: thesis: verum

end;0. (G . i) = H

then A6: H

A7: (complop G) . i = comp (G . i) by Def6;

( (carr G) . i = H

hence ( (complop G) . i is_an_inverseOp_wrt (addop G) . i & (addop G) . i is having_a_unity ) by A6, A7, PRVECT_1:2, SETWISEO:def 2; :: thesis: verum

then [:(addop G):] . (x,y) = the_unity_wrt [:(addop G):] by FINSEQOP:def 1;

hence x + y = 0. GS by A4, BINOP_1:def 8; :: thesis: verum

now :: thesis: for i being Element of dom (carr G) holds (addop G) . i is commutative

then
[:(addop G):] is commutative
by PRVECT_1:17;let i be Element of dom (carr G); :: thesis: (addop G) . i is commutative

( (addop G) . i = H_{3}(G . i) & (carr G) . i = H_{2}(G . i) )
by A1, Def5;

hence (addop G) . i is commutative by FVSUM_1:1; :: thesis: verum

end;( (addop G) . i = H

hence (addop G) . i is commutative by FVSUM_1:1; :: thesis: verum

hence ( product G is Abelian & product G is add-associative & product G is right_zeroed & product G is right_complementable & product G is vector-distributive & product G is scalar-distributive & product G is scalar-associative & product G is scalar-unital ) by A2, A4, A5, Lm1, Lm2, Lm5; :: thesis: verum