deffunc H₁( addLoopStr ) -> Element of the carrier of K = the ZeroF of K;
reconsider GS = ModuleStr(# (product (carr G)),[:(addop G):],(zeros G),[:(multop G):] #) as non empty ModuleStr over K ;
deffunc H₂( 1-sorted ) -> set = the carrier of K;
deffunc H₃( addLoopStr ) -> Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:] = the addF of K;

A1: now :: thesis: for i being Element of dom (carr G) holds (carr G) . i = H₂(G . i)

let i be Element of dom (carr G); :: thesis: (carr G) . i = H₂(G . i)
dom G = Seg (len G) by FINSEQ_1:def 3
.= Seg (len (carr G)) by PRVECT_1:def 11
.= dom (carr G) by FINSEQ_1:def 3 ;
hence (carr G) . i = H₂(G . i) by PRVECT_1:def 11; :: thesis: verum

end;

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

let i be Element of dom (carr G); :: thesis: (addop G) . i is associative
( (addop G) . i = H₃(G . i) & (carr G) . i = H₂(G . i) ) by A1, PRVECT_1:def 12;
hence (addop G) . i is associative by FVSUM_1:2; :: thesis: verum

end;

then A2: [:(addop G):] is associative by PRVECT_1:18;

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

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 PRVECT_1:def 14;
( (addop G) . i = H₃(G . i) & (carr G) . i = H₂(G . i) ) by A1, PRVECT_1:def 12;
hence (zeros G) . i is_a_unity_wrt (addop G) . i by A3, PRVECT_1:1; :: thesis: verum

end;

then A4: zeros G is_a_unity_wrt [:(addop G):] by PRVECT_1:19;
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

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 )

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 )
A6: 0. (G . i) = H₁(G . i) ;
A7: (complop G) . i = comp (G . i) by PRVECT_1:def 13;
( (carr G) . i = H₂(G . i) & (addop G) . i = H₃(G . i) ) by A1, PRVECT_1:def 12;
hence ( (complop G) . i is_an_inverseOp_wrt (addop G) . i & (addop G) . i is having_a_unity ) by A6, A7, PRVECT_1:1, PRVECT_1:2, SETWISEO:def 2; :: thesis: verum

end;

then Frege (complop G) is_an_inverseOp_wrt [:(addop G):] by PRVECT_1:20;
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;

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

let i be Element of dom (carr G); :: thesis: (addop G) . i is commutative
( (addop G) . i = H₃(G . i) & (carr G) . i = H₂(G . i) ) by A1, PRVECT_1:def 12;
hence (addop G) . i is commutative by FVSUM_1:1; :: thesis: verum

end;

then [:(addop G):] is commutative by PRVECT_1:17;
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, Lm5, BINOP_1:3; :: thesis: verum