deffunc H₁( addLoopStr ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the addF of $1;
let G be RealLinearSpace-Sequence; :: thesis:
reconsider GS = RLSStruct(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):] #) as non empty RLSStruct ;
dom G = Seg (len G) by FINSEQ_1:def 3;
then dom G = Seg (len (carr G)) by PRVECT_1:def 11;
then A1: dom G = dom (carr G) by FINSEQ_1:def 3;

now :: thesis:

let a1, b1 be Real; :: thesis:
reconsider a = a1, b = b1 as Element of REAL by XREAL_0:def 1;
let v, w be VECTOR of GS; :: thesis:
reconsider v1 = v, w1 = w as Element of product (carr G) ;

A2: now :: thesis:

let x be object ; :: thesis:
assume x in dom (carr G) ; :: thesis:
then reconsider i = x as Element of dom (carr G) ;
reconsider vi = v1 . i as VECTOR of (G . i) by A1, PRVECT_1:def 11;
([:(multop G):] . (jj,v1)) . x = 1 * vi by Lm4;
hence ([:(multop G):] . (jj,v1)) . x = v1 . x by RLVECT_1:def 8; :: thesis:

end;

A3: now :: thesis:

let x be object ; :: thesis:
assume x in dom (carr G) ; :: thesis:
then reconsider i = x as Element of dom (carr G) ;
reconsider vi = v1 . i as VECTOR of (G . i) by A1, PRVECT_1:def 11;
([:(multop G):] . ((a + b),v1)) . i = (a + b) * vi by Lm4
.= (a * vi) + (b * vi) by RLVECT_1:def 6
.= H₁(G . i) . ((([:(multop G):] . (a,v1)) . i),(b * vi)) by Lm4
.= H₁(G . i) . ((([:(multop G):] . (a,v1)) . i),(([:(multop G):] . (b,v1)) . i)) by Lm4 ;
hence ([:(multop G):] . ((a + b),v1)) . x = ([:(addop G):] . (([:(multop G):] . (a,v1)),([:(multop G):] . (b,v1)))) . x by Lm3; :: thesis:

end;

A4: now :: thesis:

let x be object ; :: thesis:
assume x in dom (carr G) ; :: thesis:
then reconsider i = x as Element of dom (carr G) ;
reconsider vi = v1 . i, wi = w1 . i as VECTOR of (G . i) by A1, PRVECT_1:def 11;
([:(multop G):] . (a,([:(addop G):] . (v1,w1)))) . i = the Mult of (G . i) . (a,(([:(addop G):] . (v1,w1)) . i)) by Lm4
.= a * (vi + wi) by Lm3
.= (a * vi) + (a * wi) by RLVECT_1:def 5
.= H₁(G . i) . ((([:(multop G):] . (a,v1)) . i),(a * wi)) by Lm4
.= H₁(G . i) . ((([:(multop G):] . (a,v1)) . i),(([:(multop G):] . (a,w1)) . i)) by Lm4 ;
hence ([:(multop G):] . (a,([:(addop G):] . (v1,w1)))) . x = ([:(addop G):] . (([:(multop G):] . (a,v1)),([:(multop G):] . (a,w1)))) . x by Lm3; :: thesis:

end;

( dom ([:(multop G):] . (a,([:(addop G):] . (v1,w1)))) = dom (carr G) & dom ([:(addop G):] . (([:(multop G):] . (a,v1)),([:(multop G):] . (a,w1)))) = dom (carr G) ) by CARD_3:9;
hence a1 * (v + w) = (a1 * v) + (a1 * w) by A4, FUNCT_1:2; :: thesis:

A5: now :: thesis:

let x be object ; :: thesis:
assume x in dom (carr G) ; :: thesis:
then reconsider i = x as Element of dom (carr G) ;
reconsider vi = v1 . i as VECTOR of (G . i) by A1, PRVECT_1:def 11;
([:(multop G):] . ((a * b),v1)) . i = (a * b) * vi by Lm4
.= a * (b * vi) by RLVECT_1:def 7
.= the Mult of (G . i) . (a,(([:(multop G):] . (b,v1)) . i)) by Lm4 ;
hence ([:(multop G):] . ((a * b),v1)) . x = ([:(multop G):] . (a,([:(multop G):] . (b,v1)))) . x by Lm4; :: thesis:

end;

( dom ([:(multop G):] . ((a + b),v1)) = dom (carr G) & dom ([:(addop G):] . (([:(multop G):] . (a,v1)),([:(multop G):] . (b,v1)))) = dom (carr G) ) by CARD_3:9;
hence (a1 + b1) * v = (a1 * v) + (b1 * v) by A3, FUNCT_1:2; :: thesis:
( dom ([:(multop G):] . ((a * b),v1)) = dom (carr G) & dom ([:(multop G):] . (a,([:(multop G):] . (b,v1)))) = dom (carr G) ) by CARD_3:9;
hence (a1 * b1) * v = a1 * (b1 * v) by A5, FUNCT_1:2; :: thesis:
( dom ([:(multop G):] . (jj,v1)) = dom (carr G) & dom v1 = dom (carr G) ) by CARD_3:9;
hence 1 * v = v by A2, FUNCT_1:2; :: thesis:

end;

hence ( product G is vector-distributive & product G is scalar-distributive & product G is scalar-associative & product G is scalar-unital ) ; :: thesis: