let RS be RealLinearSpace; :: thesis: for f being FinSequence of RS
for x, y being Element of RS
for a, b being Integer 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 Integer 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 Integer st x in Z_Lin f & y in Z_Lin f holds
(a * x) + (b * y) in Z_Lin f
let a, b be Integer; :: thesis: ( x in Z_Lin f & y in Z_Lin f implies (a * x) + (b * y) in Z_Lin f )
assume A1: ( x in Z_Lin f & y in Z_Lin f ) ; :: thesis: (a * x) + (b * y) in Z_Lin f
consider g being len f -element FinSequence of RS, s being INT -valued len f -element FinSequence such that
A2: ( x = Sum g & ( for i being Nat st i in Seg (len f) holds
g /. i = (s . i) * (f /. i) ) ) by A1, Th26;
consider h being len f -element FinSequence of RS, t being INT -valued len f -element FinSequence such that
A3: ( y = Sum h & ( for i being Nat st i in Seg (len f) holds
h /. i = (t . i) * (f /. i) ) ) by A1, Th26;
defpred S₁[ Nat, set ] means $2 = (a * (s . $1)) + (b * (t . $1));
A4: for k being Nat st k in Seg (len f) holds
ex x being Element of INT st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (len f) implies ex x being Element of INT st S₁[k,x] )
assume k in Seg (len f) ; :: thesis: ex x being Element of INT st S₁[k,x]
reconsider x = (a * (s . k)) + (b * (t . k)) as Element of INT by INT_1:def 2;
take x ; :: thesis: S₁[k,x]
thus S₁[k,x] ; :: thesis: verum

end;

consider u being FinSequence of INT such that
A5: ( 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(A4);
len u = len f by A5, FINSEQ_1:def 3;
then reconsider u = u as INT -valued len f -element FinSequence by CARD_1:def 7;
defpred S₂[ Nat, set ] means $2 = (a * (g /. $1)) + (b * (h /. $1));
A6: 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
A7: ( 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(A6);
len w = len f by A7, FINSEQ_1:def 3;
then reconsider w = w as len f -element FinSequence of RS by CARD_1:def 7;

A8: now :: thesis: for i being Nat st i in Seg (len f) holds
w /. i = (a * (g /. i)) + (b * (h /. i))

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

end;

a in INT by INT_1:def 2;
then reconsider a0 = a as Element of REAL by NUMBERS:15;
b in INT by INT_1:def 2;
then reconsider b0 = b as Element of REAL by NUMBERS:15;
dom (a0 (#) g) = dom g by VFUNCT_1:def 4
.= Seg (len g) by FINSEQ_1:def 3 ;
then A10: a0 (#) g is FinSequence-like ;
rng (a0 (#) g) c= the carrier of RS ;
then reconsider ag = a0 (#) g as FinSequence of RS by A10, FINSEQ_1:def 4;
dom (b0 (#) h) = dom h by VFUNCT_1:def 4
.= Seg (len h) by FINSEQ_1:def 3 ;
then A11: b0 (#) h is FinSequence-like ;
rng (b0 (#) h) c= the carrier of RS ;
then reconsider bh = b0 (#) h as FinSequence of RS by A11, FINSEQ_1:def 4;
A12: dom (a0 (#) g) = dom g by VFUNCT_1:def 4
.= Seg (len g) by FINSEQ_1:def 3
.= Seg (len f) by CARD_1:def 7 ;
then A13: len ag = len f by FINSEQ_1:def 3;
A14: dom (b0 (#) h) = dom h by VFUNCT_1:def 4
.= Seg (len h) by FINSEQ_1:def 3
.= Seg (len f) by CARD_1:def 7 ;

A15: now :: thesis: for i being Nat st i in dom ag holds
w . i = (ag /. i) + (bh /. i)

let i be Nat; :: thesis: ( i in dom ag implies w . i = (ag /. i) + (bh /. i) )
assume A16: i in dom ag ; :: thesis: w . i = (ag /. i) + (bh /. i)
hence w . i = (a * (g /. i)) + (b * (h /. i)) by A7, A12
.= (ag /. i) + (b * (h /. i)) by A16, VFUNCT_1:def 4
.= (ag /. i) + (bh /. i) by A16, A14, A12, VFUNCT_1:def 4 ;
:: thesis: verum

end;

A17: ( len ag = len bh & len ag = len w ) by A7, A13, A14, FINSEQ_1:def 3;
A18: 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 A19: i in Seg (len f) ; :: thesis: w /. i = (u . i) * (f /. i)
hence w /. i = (a * (g /. i)) + (b * (h /. i)) by A8
.= (a * ((s . i) * (f /. i))) + (b * (h /. i)) by A19, A2
.= (a * ((s . i) * (f /. i))) + (b * ((t . i) * (f /. i))) by A19, A3
.= ((a * (s . i)) * (f /. i)) + (b * ((t . i) * (f /. i))) by RLVECT_1:def 7
.= ((a * (s . i)) * (f /. i)) + ((b * (t . i)) * (f /. i)) by RLVECT_1:def 7
.= ((a * (s . i)) + (b * (t . i))) * (f /. i) by RLVECT_1:def 6
.= (u . i) * (f /. i) by A19, A5 ;
:: thesis: verum

end;

(a * x) + (b * y) = (Sum ag) + (b * (Sum h)) by A2, A3, Th3
.= (Sum ag) + (Sum bh) by Th3
.= Sum w by A15, A17, RLVECT_2:2 ;
hence (a * x) + (b * y) in Z_Lin f by A18; :: thesis: verum