let m, n be Element of NAT ; :: thesis: for f being LinearOperator of m,n
for xseq being FinSequence of REAL m
for yseq being FinSequence of REAL n st len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
yseq . i = f . (xseq . i) ) holds
Sum yseq = f . (Sum xseq)
let f be LinearOperator of m,n; :: thesis: for xseq being FinSequence of REAL m
for yseq being FinSequence of REAL n st len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
yseq . i = f . (xseq . i) ) holds
Sum yseq = f . (Sum xseq)
defpred S₁[ Nat] means for xseq being FinSequence of REAL m
for yseq being FinSequence of REAL n st $1 = len xseq & len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
yseq . i = f . (xseq . i) ) holds
Sum yseq = f . (Sum xseq);
P0: S₁[ 0 ]

proof

let xseq be FinSequence of REAL m; :: thesis: for yseq being FinSequence of REAL n st 0 = len xseq & len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
yseq . i = f . (xseq . i) ) holds
Sum yseq = f . (Sum xseq)
let yseq be FinSequence of REAL n; :: thesis: ( 0 = len xseq & len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
yseq . i = f . (xseq . i) ) implies Sum yseq = f . (Sum xseq) )
assume ( 0 = len xseq & len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
yseq . i = f . (xseq . i) ) ) ; :: thesis: Sum yseq = f . (Sum xseq)
then ( Sum xseq = 0* m & Sum yseq = 0* n ) by EUCLID_7:def 11;
hence Sum yseq = f . (Sum xseq) by SSS1; :: thesis: verum

end;

P1: now

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume AS1: S₁[i] ; :: thesis: S₁[i + 1]

now

let xseq be FinSequence of REAL m; :: thesis: for yseq being FinSequence of REAL n st i + 1 = len xseq & len xseq = len yseq & ( for k being Element of NAT st k in dom xseq holds
yseq . k = f . (xseq . k) ) holds
Sum yseq = f . (Sum xseq)
let yseq be FinSequence of REAL n; :: thesis: ( i + 1 = len xseq & len xseq = len yseq & ( for k being Element of NAT st k in dom xseq holds
yseq . k = f . (xseq . k) ) implies Sum yseq = f . (Sum xseq) )
assume P01: ( i + 1 = len xseq & len xseq = len yseq & ( for k being Element of NAT st k in dom xseq holds
yseq . k = f . (xseq . k) ) ) ; :: thesis: Sum yseq = f . (Sum xseq)
set xseq0 = xseq | i;
set yseq0 = yseq | i;
P02: i = len (xseq | i) by P01, FINSEQ_1:80, NAT_1:11;
then P03: len (xseq | i) = len (yseq | i) by P01, FINSEQ_1:80, NAT_1:11;
for k being Element of NAT st k in dom (xseq | i) holds
(yseq | i) . k = f . ((xseq | i) . k)

proof

let k be Element of NAT ; :: thesis: ( k in dom (xseq | i) implies (yseq | i) . k = f . ((xseq | i) . k) )
assume AA2: k in dom (xseq | i) ; :: thesis: (yseq | i) . k = f . ((xseq | i) . k)
then AA4: k in Seg i by RELAT_1:86;
k in dom xseq by AA2, RELAT_1:86;
then AA5: yseq . k = f . (xseq . k) by P01;
xseq . k = (xseq | i) . k by AA4, FUNCT_1:72;
hence (yseq | i) . k = f . ((xseq | i) . k) by AA4, AA5, FUNCT_1:72; :: thesis: verum

end;

then XXX1: Sum (yseq | i) = f . (Sum (xseq | i)) by P02, P03, AS1;
consider v being Element of REAL m such that
P071: ( v = xseq . (len xseq) & Sum xseq = (Sum (xseq | i)) + v ) by P01, P02, LOPBTh2581;
consider w being Element of REAL n such that
P07A1: ( w = yseq . (len yseq) & Sum yseq = (Sum (yseq | i)) + w ) by P01, P02, P03, LOPBTh2581;
dom xseq = Seg (i + 1) by P01, FINSEQ_1:def 3;
then w = f . v by P01, P07A1, P071, FINSEQ_1:6;
hence Sum yseq = f . (Sum xseq) by XXX1, P071, P07A1, LOPBDef5; :: thesis: verum

end;

hence S₁[i + 1] ; :: thesis: verum

end;

P2: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(P0, P1);
let xseq be FinSequence of REAL m; :: thesis: for yseq being FinSequence of REAL n st len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
yseq . i = f . (xseq . i) ) holds
Sum yseq = f . (Sum xseq)
let yseq be FinSequence of REAL n; :: thesis: ( len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
yseq . i = f . (xseq . i) ) implies Sum yseq = f . (Sum xseq) )
assume ( len xseq = len yseq & ( for i being Element of NAT st i in dom xseq holds
yseq . i = f . (xseq . i) ) ) ; :: thesis: Sum yseq = f . (Sum xseq)
hence Sum yseq = f . (Sum xseq) by P2; :: thesis: verum