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

A1: now

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 Def4
.= dom (carr G) by FINSEQ_1:def 3 ;
hence (carr G) . i = H₂(G . i) by Def4; :: thesis: verum

end;

now

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, Def5;
hence (addop G) . i is commutative by FVSUM_1:2; :: thesis: verum

end;

then A2: [:(addop G):] is commutative by PRVECT_1:25;

now

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, Def5;
hence (addop G) . i is associative by FVSUM_1:3; :: thesis: verum

end;

then A3: [:(addop G):] is associative by PRVECT_1:26;
deffunc H₃( addLoopStr ) -> Element of the carrier of G = the ZeroF of G;

now

let i be Element of dom (carr G); :: thesis: (zeros G) . i is_a_unity_wrt (addop G) . i
A4: ( (addop G) . i = H₁(G . i) & (zeros G) . i = H₃(G . i) & (carr G) . i = H₂(G . i) ) by A1, Def5, Def7;
(zeros G) . i = 0. (G . i) by Def7;
hence (zeros G) . i is_a_unity_wrt (addop G) . i by A4, PRVECT_1:3; :: thesis: verum

end;

then A5: zeros G is_a_unity_wrt [:(addop G):] by PRVECT_1:27;
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:7;
take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. GS

now

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₃(G . i) ;
then ( H₃(G . i) is_a_unity_wrt H₁(G . i) & (carr G) . i = H₂(G . i) & (addop G) . i = H₁(G . i) & (complop G) . i = comp (G . i) ) by A1, Def5, Def6, PRVECT_1:3;
hence ( (complop G) . i is_an_inverseOp_wrt (addop G) . i & (addop G) . i is having_a_unity ) by PRVECT_1:4, SETWISEO:def 2; :: thesis: verum

end;

then Frege (complop G) is_an_inverseOp_wrt [:(addop G):] by PRVECT_1:28;
then [:(addop G):] . x,y = the_unity_wrt [:(addop G):] by FINSEQOP:def 1;
hence x + y = 0. GS by A5, BINOP_1:def 8; :: thesis: verum

end;

hence ( product G is Abelian & product G is add-associative & product G is right_zeroed & product G is right_complementable & product G is RealLinearSpace-like ) by A2, A3, A5, Lm1, Lm2, Lm5; :: thesis: verum