let RS be RealLinearSpace; :: thesis: for f being FinSequence of RS
for x, y being Element of RS
for a, b being Element of INT st x in Z_Lin f & y in Z_Lin f holds
(a * x) + (b * y) in Z_Lin f
let f be FinSequence of RS; :: thesis: for x, y being Element of RS
for a, b being Element of INT st x in Z_Lin f & y in Z_Lin f holds
(a * x) + (b * y) in Z_Lin f
let x, y be Element of RS; :: thesis: for a, b being Element of INT st x in Z_Lin f & y in Z_Lin f holds
(a * x) + (b * y) in Z_Lin f
let a, b be Element of INT ; :: thesis: ( x in Z_Lin f & y in Z_Lin f implies (a * x) + (b * y) in Z_Lin f )
assume AS: ( x in Z_Lin f & y in Z_Lin f ) ; :: thesis: (a * x) + (b * y) in Z_Lin f
consider g being len f -long FinSequence of RS, s being len f -long integer-valued FinSequence such that
P1: ( x = Sum g & ( for i being Nat st i in Seg (len f) holds
g /. i = (s . i) * (f /. i) ) ) by AS, SLM001;
consider h being len f -long FinSequence of RS, t being len f -long integer-valued FinSequence such that
P2: ( y = Sum h & ( for i being Nat st i in Seg (len f) holds
h /. i = (t . i) * (f /. i) ) ) by AS, SLM001;
defpred S₁[ Nat, set ] means $2 = (a * (s . $1)) + (b * (t . $1));
D2: for k being Nat st k in Seg (len f) holds
ex x being Element of INT st S₁[k,x] ;
consider u being FinSequence of INT such that
X0: ( dom u = Seg (len f) & ( for i being Nat st i in Seg (len f) holds
S₁[i,u . i] ) ) from FINSEQ_1:sch 5(D2);
len u = len f by X0, FINSEQ_1:def 3;
then reconsider u = u as len f -long integer-valued FinSequence by FINSEQ_1:def 18;
defpred S₂[ Nat, set ] means $2 = (a * (g /. $1)) + (b * (h /. $1));
D1: for k being Nat st k in Seg (len f) holds
ex x being Element of RS st S₂[k,x] ;
consider w being FinSequence of RS such that
X01: ( dom w = Seg (len f) & ( for i being Nat st i in Seg (len f) holds
S₂[i,w . i] ) ) from FINSEQ_1:sch 5(D1);
len w = len f by X01, FINSEQ_1:def 3;
then reconsider w = w as len f -long FinSequence of RS by FINSEQ_1:def 18;

X1: now

let i be Nat; :: thesis: ( i in Seg (len f) implies w /. i = (a * (g /. i)) + (b * (h /. i)) )
assume A1: i in Seg (len f) ; :: thesis: w /. i = (a * (g /. i)) + (b * (h /. i))
hence w /. i = w . i by X01, PARTFUN1:def 8
.= (a * (g /. i)) + (b * (h /. i)) by X01, A1 ;
:: thesis: verum

end;

reconsider a0 = a as Element of REAL by NUMBERS:15, TARSKI:def 3;
reconsider b0 = b as Element of REAL by NUMBERS:15, TARSKI:def 3;
dom (a0 (#) g) = dom g by VFUNCT_1:def 4
.= Seg (len g) by FINSEQ_1:def 3 ;
then Y2: a0 (#) g is FinSequence-like by FINSEQ_1:def 2;
rng (a0 (#) g) c= the carrier of RS ;
then reconsider ag = a0 (#) g as FinSequence of RS by Y2, FINSEQ_1:def 4;
dom (b0 (#) h) = dom h by VFUNCT_1:def 4
.= Seg (len h) by FINSEQ_1:def 3 ;
then Y4: b0 (#) h is FinSequence-like by FINSEQ_1:def 2;
rng (b0 (#) h) c= the carrier of RS ;
then reconsider bh = b0 (#) h as FinSequence of RS by Y4, FINSEQ_1:def 4;
H5: dom (a0 (#) g) = dom g by VFUNCT_1:def 4
.= Seg (len g) by FINSEQ_1:def 3
.= Seg (len f) by FINSEQ_1:def 18 ;
then H1: len ag = len f by FINSEQ_1:def 3;
H3: dom (b0 (#) h) = dom h by VFUNCT_1:def 4
.= Seg (len h) by FINSEQ_1:def 3
.= Seg (len f) by FINSEQ_1:def 18 ;

X4: now

let i be Element of NAT ; :: thesis: ( i in dom ag implies w . i = (ag /. i) + (bh /. i) )
assume D0: i in dom ag ; :: thesis: w . i = (ag /. i) + (bh /. i)
hence w . i = (a * (g /. i)) + (b * (h /. i)) by X01, H5
.= (ag /. i) + (b * (h /. i)) by D0, VFUNCT_1:def 4
.= (ag /. i) + (bh /. i) by D0, H3, H5, VFUNCT_1:def 4 ;
:: thesis: verum

end;

X5: ( len ag = len bh & len ag = len w ) by X01, H1, H3, FINSEQ_1:def 3;
P4: for i being Nat st i in Seg (len f) holds
w /. i = (u . i) * (f /. i)

proof

let i be Nat; :: thesis: ( i in Seg (len f) implies w /. i = (u . i) * (f /. i) )
assume AS1: i in Seg (len f) ; :: thesis: w /. i = (u . i) * (f /. i)
hence w /. i = (a * (g /. i)) + (b * (h /. i)) by X1
.= (a * ((s . i) * (f /. i))) + (b * (h /. i)) by AS1, P1
.= (a * ((s . i) * (f /. i))) + (b * ((t . i) * (f /. i))) by AS1, P2
.= ((a * (s . i)) * (f /. i)) + (b * ((t . i) * (f /. i))) by RLVECT_1:def 10
.= ((a * (s . i)) * (f /. i)) + ((b * (t . i)) * (f /. i)) by RLVECT_1:def 10
.= ((a * (s . i)) + (b * (t . i))) * (f /. i) by RLVECT_1:def 9
.= (u . i) * (f /. i) by AS1, X0 ;
:: thesis: verum

end;

(a * x) + (b * y) = (Sum ag) + (b * (Sum h)) by P1, P2, SM3
.= (Sum ag) + (Sum bh) by SM3
.= Sum w by X4, X5, RLVECT_2:4 ;
hence (a * x) + (b * y) in Z_Lin f by P4; :: thesis: verum