let K be Ring; :: thesis: for G being VectorSpace-Sequence of K holds
( product G is vector-distributive & product G is scalar-distributive & product G is scalar-associative & product G is scalar-unital )
let G be VectorSpace-Sequence of K; :: thesis: ( product G is vector-distributive & product G is scalar-distributive & product G is scalar-associative & product G is scalar-unital )
deffunc H₁( addLoopStr ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the addF of $1;
reconsider GS = ModuleStr(# (product (carr G)),[:(addop G):],(zeros G),[:(multop G):] #) as non empty ModuleStr over K ;
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: for a, b being Element of K
for v, w being Vector of GS holds
( a * (v + w) = (a * v) + (a * w) & (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & (1. K) * v = v )

let a, b be Element of K; :: thesis: for v, w being Vector of GS holds
( a * (v + w) = (a * v) + (a * w) & (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & (1. K) * v = v )
let v, w be Vector of GS; :: thesis: ( a * (v + w) = (a * v) + (a * w) & (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & (1. K) * 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
([:(multop G):] . ((1. K),v1)) . x = v1 . x

let x be object ; :: thesis: ( x in dom (carr G) implies ([:(multop G):] . ((1. K),v1)) . x = v1 . x )
assume x in dom (carr G) ; :: thesis: ([:(multop G):] . ((1. K),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, PRVECT_1:def 11;
([:(multop G):] . ((1. K),v1)) . x = (1. K) * vi by Lm4;
hence ([:(multop G):] . ((1. K),v1)) . x = v1 . x ; :: thesis: verum

end;

A3: now :: thesis: for x being object st x in dom (carr G) holds
([:(multop G):] . ((a + b),v1)) . x = ([:(addop G):] . (([:(multop G):] . (a,v1)),([:(multop G):] . (b,v1)))) . x

let x be object ; :: 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, PRVECT_1:def 11;
([:(multop G):] . ((a + b),v1)) . i = (a + b) * vi by Lm4
.= (a * vi) + (b * vi) by VECTSP_1:def 15
.= 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;

A4: now :: thesis: for x being object st x in dom (carr G) holds
([:(multop G):] . (a,([:(addop G):] . (v1,w1)))) . x = ([:(addop G):] . (([:(multop G):] . (a,v1)),([:(multop G):] . (a,w1)))) . x

let x be object ; :: 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, PRVECT_1:def 11;
([:(multop G):] . (a,([:(addop G):] . (v1,w1)))) . i = the lmult of (G . i) . (a,(([:(addop G):] . (v1,w1)) . i)) by Lm4
.= a * (vi + wi) by Lm3
.= (a * vi) + (a * wi) by VECTSP_1:def 14
.= 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;

( 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 a * (v + w) = (a * v) + (a * w) by A4, FUNCT_1:2; :: thesis: ( (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & (1. K) * v = v )

A5: now :: thesis: for x being object st x in dom (carr G) holds
([:(multop G):] . ((a * b),v1)) . x = ([:(multop G):] . (a,([:(multop G):] . (b,v1)))) . x

let x be object ; :: 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, PRVECT_1:def 11;
([:(multop G):] . ((a * b),v1)) . i = (a * b) * vi by Lm4
.= a * (b * vi) by VECTSP_1:def 16
.= the lmult 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;

( 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 (a + b) * v = (a * v) + (b * v) by A3, FUNCT_1:2; :: thesis: ( (a * b) * v = a * (b * v) & (1. K) * v = v )
( 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 (a * b) * v = a * (b * v) by A5, FUNCT_1:2; :: thesis: (1. K) * v = v
( dom ([:(multop G):] . ((1. K),v1)) = dom (carr G) & dom v1 = dom (carr G) ) by CARD_3:9;
hence (1. K) * v = v by A2, FUNCT_1:2; :: 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