let G be RealLinearSpace-Sequence; :: thesis: product G is RealLinearSpace-like
deffunc H₁( addLoopStr ) -> Element of bool [:[:the carrier of $1,the carrier of $1:],the carrier of $1:] = the addF of $1;
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 Def4;
then A1: dom G = dom (carr G) by FINSEQ_1:def 3;

now

let a1, b1 be real number ; :: 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 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: ( 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) & dom ([:(multop G):] . (a + b),v1) = dom (carr G) & dom ([:(addop G):] . ([:(multop G):] . a,v1),([:(multop G):] . b,v1)) = dom (carr G) & dom ([:(multop G):] . (a * b),v1) = dom (carr G) & dom ([:(multop G):] . a,([:(multop G):] . b,v1)) = dom (carr G) & dom ([:(multop G):] . 1,v1) = dom (carr G) & dom v1 = dom (carr G) ) by CARD_3:18;

now

let x be set ; :: thesis: ( x in dom (carr G) implies ([:(multop G):] . a,([:(addop G):] . v1,w1)) . x = ([:(addop G):] . ([:(multop G):] . a,v1),([:(multop G):] . a,w1)) . x )
assume x in dom (carr G) ; :: thesis: ([:(multop G):] . a,([:(addop G):] . v1,w1)) . x = ([:(addop G):] . ([:(multop G):] . a,v1),([:(multop G):] . 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 A1, Def4;
([:(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 9
.= 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: verum

end;

hence a1 * (v + w) = (a1 * v) + (a1 * w) by A2, FUNCT_1:9; :: thesis: ( (a1 + b1) * v = (a1 * v) + (b1 * v) & (a1 * b1) * v = a1 * (b1 * v) & 1 * v = v )

now

let x be set ; :: thesis: ( x in dom (carr G) implies ([:(multop G):] . (a + b),v1) . x = ([:(addop G):] . ([:(multop G):] . a,v1),([:(multop G):] . b,v1)) . x )
assume x in dom (carr G) ; :: thesis: ([:(multop G):] . (a + b),v1) . x = ([:(addop G):] . ([:(multop G):] . a,v1),([:(multop G):] . b,v1)) . x
then reconsider i = x as Element of dom (carr G) ;
reconsider vi = v1 . i as VECTOR of (G . i) by A1, Def4;
([:(multop G):] . (a + b),v1) . i = (a + b) * vi by Lm4
.= (a * vi) + (b * vi) by RLVECT_1:def 9
.= 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: verum

end;

hence (a1 + b1) * v = (a1 * v) + (b1 * v) by A2, FUNCT_1:9; :: thesis: ( (a1 * b1) * v = a1 * (b1 * v) & 1 * v = v )

now

let x be set ; :: thesis: ( x in dom (carr G) implies ([:(multop G):] . (a * b),v1) . x = ([:(multop G):] . a,([:(multop G):] . b,v1)) . x )
assume x in dom (carr G) ; :: thesis: ([:(multop G):] . (a * b),v1) . x = ([:(multop G):] . a,([:(multop G):] . b,v1)) . x
then reconsider i = x as Element of dom (carr G) ;
reconsider vi = v1 . i as VECTOR of (G . i) by A1, Def4;
([:(multop G):] . (a * b),v1) . i = (a * b) * vi by Lm4
.= a * (b * vi) by RLVECT_1:def 9
.= 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: verum

end;

hence (a1 * b1) * v = a1 * (b1 * v) by A2, FUNCT_1:9; :: thesis: 1 * v = v

now

let x be set ; :: thesis: ( x in dom (carr G) implies ([:(multop G):] . 1,v1) . x = v1 . x )
assume x in dom (carr G) ; :: thesis: ([:(multop G):] . 1,v1) . x = v1 . x
then reconsider i = x as Element of dom (carr G) ;
reconsider vi = v1 . i as VECTOR of (G . i) by A1, Def4;
([:(multop G):] . 1,v1) . x = 1 * vi by Lm4;
hence ([:(multop G):] . 1,v1) . x = v1 . x by RLVECT_1:def 9; :: thesis: verum

end;

hence 1 * v = v by A2, FUNCT_1:9; :: thesis: verum

end;

hence product G is RealLinearSpace-like by RLVECT_1:def 9; :: thesis: verum