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; ( product G is vector-distributive & product G is scalar-distributive & product G is scalar-associative & product G is scalar-unital )
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 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;
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;
( 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) ;
A3:
now 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)))) . xlet x be
object ;
( 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)
;
([:(multop G):] . ((a + b),v1)) . x = ([:(addop G):] . (([:(multop G):] . (a,v1)),([:(multop G):] . (b,v1)))) . xthen 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
.=
H1(
G . i)
. (
(([:(multop G):] . (a,v1)) . i),
(b * vi))
by Lm4
.=
H1(
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;
verum end; A4:
now 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)))) . xlet x be
object ;
( 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)
;
([:(multop G):] . (a,([:(addop G):] . (v1,w1)))) . x = ([:(addop G):] . (([:(multop G):] . (a,v1)),([:(multop G):] . (a,w1)))) . xthen 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
.=
H1(
G . i)
. (
(([:(multop G):] . (a,v1)) . i),
(a * wi))
by Lm4
.=
H1(
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;
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
a1 * (v + w) = (a1 * v) + (a1 * w)
by A4, FUNCT_1:2;
( (a1 + b1) * v = (a1 * v) + (b1 * v) & (a1 * b1) * v = a1 * (b1 * v) & 1 * v = v )A5:
now for x being object st x in dom (carr G) holds
([:(multop G):] . ((a * b),v1)) . x = ([:(multop G):] . (a,([:(multop G):] . (b,v1)))) . xlet x be
object ;
( 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)
;
([:(multop G):] . ((a * b),v1)) . x = ([:(multop G):] . (a,([:(multop G):] . (b,v1)))) . xthen 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;
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
(a1 + b1) * v = (a1 * v) + (b1 * v)
by A3, FUNCT_1:2;
( (a1 * b1) * v = a1 * (b1 * v) & 1 * 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
(a1 * b1) * v = a1 * (b1 * v)
by A5, FUNCT_1:2;
1 * v = v
(
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;
verum end;
hence
( product G is vector-distributive & product G is scalar-distributive & product G is scalar-associative & product G is scalar-unital )
; verum