deffunc H1( 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)),(),[:():],[:():] #) as non empty RLSStruct ;
dom G = Seg (len G) by FINSEQ_1:def 3;
then dom G = Seg (len (carr G)) by Def4;
then A1: dom G = dom (carr G) by FINSEQ_1:def 3;
now :: thesis: for a1, b1 being Real
for v, w being VECTOR of GS holds
( a1 * (v + w) = (a1 * v) + (a1 * w) & (a1 + b1) * v = (a1 * v) + (b1 * v) & (a1 * b1) * v = a1 * (b1 * v) & 1 * v = v )
let a1, b1 be Real; :: thesis: for v, w being VECTOR of GS holds
( a1 * (v + w) = (a1 * v) + (a1 * w) & (a1 + b1) * v = (a1 * v) + (b1 * v) & (a1 * b1) * v = a1 * (b1 * v) & 1 * v = v )

reconsider a = a1, b = b1 as Element of REAL by XREAL_0:def 1;
let v, w be VECTOR of GS; :: thesis: ( a1 * (v + w) = (a1 * v) + (a1 * w) & (a1 + b1) * v = (a1 * v) + (b1 * v) & (a1 * b1) * v = a1 * (b1 * v) & 1 * v = v )
reconsider v1 = v, w1 = w as Element of product (carr G) ;
A2: now :: thesis: for x being object st x in dom (carr G) holds
([:():] . (jj,v1)) . x = v1 . x
let x be object ; :: thesis: ( x in dom (carr G) implies ([:():] . (jj,v1)) . x = v1 . x )
assume x in dom (carr G) ; :: thesis: ([:():] . (jj,v1)) . x = v1 . x
then reconsider i = x as Element of dom (carr G) ;
reconsider vi = v1 . i as VECTOR of (G . i) by ;
([:():] . (jj,v1)) . x = 1 * vi by Lm4;
hence ([:():] . (jj,v1)) . x = v1 . x by RLVECT_1:def 8; :: thesis: verum
end;
A3: now :: thesis: for x being object st x in dom (carr G) holds
([:():] . ((a + b),v1)) . x = ([:():] . (([:():] . (a,v1)),([:():] . (b,v1)))) . x
let x be object ; :: thesis: ( x in dom (carr G) implies ([:():] . ((a + b),v1)) . x = ([:():] . (([:():] . (a,v1)),([:():] . (b,v1)))) . x )
assume x in dom (carr G) ; :: thesis: ([:():] . ((a + b),v1)) . x = ([:():] . (([:():] . (a,v1)),([:():] . (b,v1)))) . x
then reconsider i = x as Element of dom (carr G) ;
reconsider vi = v1 . i as VECTOR of (G . i) by ;
([:():] . ((a + b),v1)) . i = (a + b) * vi by Lm4
.= (a * vi) + (b * vi) by RLVECT_1:def 6
.= H1(G . i) . ((([:():] . (a,v1)) . i),(b * vi)) by Lm4
.= H1(G . i) . ((([:():] . (a,v1)) . i),(([:():] . (b,v1)) . i)) by Lm4 ;
hence ([:():] . ((a + b),v1)) . x = ([:():] . (([:():] . (a,v1)),([:():] . (b,v1)))) . x by Lm3; :: thesis: verum
end;
A4: now :: thesis: for x being object st x in dom (carr G) holds
([:():] . (a,([:():] . (v1,w1)))) . x = ([:():] . (([:():] . (a,v1)),([:():] . (a,w1)))) . x
let x be object ; :: thesis: ( x in dom (carr G) implies ([:():] . (a,([:():] . (v1,w1)))) . x = ([:():] . (([:():] . (a,v1)),([:():] . (a,w1)))) . x )
assume x in dom (carr G) ; :: thesis: ([:():] . (a,([:():] . (v1,w1)))) . x = ([:():] . (([:():] . (a,v1)),([:():] . (a,w1)))) . x
then reconsider i = x as Element of dom (carr G) ;
reconsider vi = v1 . i, wi = w1 . i as VECTOR of (G . i) by ;
([:():] . (a,([:():] . (v1,w1)))) . i = the Mult of (G . i) . (a,(([:():] . (v1,w1)) . i)) by Lm4
.= a * (vi + wi) by Lm3
.= (a * vi) + (a * wi) by RLVECT_1:def 5
.= H1(G . i) . ((([:():] . (a,v1)) . i),(a * wi)) by Lm4
.= H1(G . i) . ((([:():] . (a,v1)) . i),(([:():] . (a,w1)) . i)) by Lm4 ;
hence ([:():] . (a,([:():] . (v1,w1)))) . x = ([:():] . (([:():] . (a,v1)),([:():] . (a,w1)))) . x by Lm3; :: thesis: verum
end;
( dom ([:():] . (a,([:():] . (v1,w1)))) = dom (carr G) & dom ([:():] . (([:():] . (a,v1)),([:():] . (a,w1)))) = dom (carr G) ) by CARD_3:9;
hence a1 * (v + w) = (a1 * v) + (a1 * w) by ; :: thesis: ( (a1 + b1) * v = (a1 * v) + (b1 * v) & (a1 * b1) * v = a1 * (b1 * v) & 1 * v = v )
A5: now :: thesis: for x being object st x in dom (carr G) holds
([:():] . ((a * b),v1)) . x = ([:():] . (a,([:():] . (b,v1)))) . x
let x be object ; :: thesis: ( x in dom (carr G) implies ([:():] . ((a * b),v1)) . x = ([:():] . (a,([:():] . (b,v1)))) . x )
assume x in dom (carr G) ; :: thesis: ([:():] . ((a * b),v1)) . x = ([:():] . (a,([:():] . (b,v1)))) . x
then reconsider i = x as Element of dom (carr G) ;
reconsider vi = v1 . i as VECTOR of (G . i) by ;
([:():] . ((a * b),v1)) . i = (a * b) * vi by Lm4
.= a * (b * vi) by RLVECT_1:def 7
.= the Mult of (G . i) . (a,(([:():] . (b,v1)) . i)) by Lm4 ;
hence ([:():] . ((a * b),v1)) . x = ([:():] . (a,([:():] . (b,v1)))) . x by Lm4; :: thesis: verum
end;
( dom ([:():] . ((a + b),v1)) = dom (carr G) & dom ([:():] . (([:():] . (a,v1)),([:():] . (b,v1)))) = dom (carr G) ) by CARD_3:9;
hence (a1 + b1) * v = (a1 * v) + (b1 * v) by ; :: thesis: ( (a1 * b1) * v = a1 * (b1 * v) & 1 * v = v )
( dom ([:():] . ((a * b),v1)) = dom (carr G) & dom ([:():] . (a,([:():] . (b,v1)))) = dom (carr G) ) by CARD_3:9;
hence (a1 * b1) * v = a1 * (b1 * v) by ; :: thesis: 1 * v = v
( dom ([:():] . (jj,v1)) = dom (carr G) & dom v1 = dom (carr G) ) by CARD_3:9;
hence 1 * v = v by ; :: thesis: verum
end;
hence ( product G is vector-distributive & product G is scalar-distributive & product G is scalar-associative & product G is scalar-unital ) ; :: thesis: verum