let n, m be 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 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 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 Nat st i in dom xseq holds
yseq . i = f . (xseq . i) ) holds
Sum yseq = f . (Sum xseq);
A1: 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 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 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 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 Th11; :: thesis: verum

end;

A2: now :: thesis: for i being Nat st S₁[i] holds
S₁[i + 1]

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A3: S₁[i] ; :: thesis: S₁[i + 1]

now :: thesis: for xseq being FinSequence of REAL m
for yseq being FinSequence of REAL n st i + 1 = len xseq & len xseq = len yseq & ( for k being Nat st k in dom xseq holds
yseq . k = f . (xseq . k) ) holds
Sum yseq = f . (Sum xseq)

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 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 Nat st k in dom xseq holds
yseq . k = f . (xseq . k) ) implies Sum yseq = f . (Sum xseq) )
assume A4: ( i + 1 = len xseq & len xseq = len yseq & ( for k being 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;
A5: i = len (xseq | i) by A4, FINSEQ_1:59, NAT_1:11;
then A6: len (xseq | i) = len (yseq | i) by A4, FINSEQ_1:59, NAT_1:11;
for k being Nat st k in dom (xseq | i) holds
(yseq | i) . k = f . ((xseq | i) . k)

proof

let k be Nat; :: thesis: ( k in dom (xseq | i) implies (yseq | i) . k = f . ((xseq | i) . k) )
assume A7: k in dom (xseq | i) ; :: thesis: (yseq | i) . k = f . ((xseq | i) . k)
then A8: k in Seg i by RELAT_1:57;
k in dom xseq by A7, RELAT_1:57;
then A9: yseq . k = f . (xseq . k) by A4;
xseq . k = (xseq | i) . k by A8, FUNCT_1:49;
hence (yseq | i) . k = f . ((xseq | i) . k) by A8, A9, FUNCT_1:49; :: thesis: verum

end;

then A10: Sum (yseq | i) = f . (Sum (xseq | i)) by A5, A6, A3;
consider v being Element of REAL m such that
A11: ( v = xseq . (len xseq) & Sum xseq = (Sum (xseq | i)) + v ) by A4, A5, Th15;
consider w being Element of REAL n such that
A12: ( w = yseq . (len yseq) & Sum yseq = (Sum (yseq | i)) + w ) by A4, A5, A6, Th15;
dom xseq = Seg (i + 1) by A4, FINSEQ_1:def 3;
then w = f . v by A4, A12, A11, FINSEQ_1:4;
hence Sum yseq = f . (Sum xseq) by A10, A11, A12, Def1; :: thesis: verum

end;

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

end;

A13: for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
let xseq be FinSequence of REAL m; :: thesis: for yseq being FinSequence of REAL n st len xseq = len yseq & ( for i being 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 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 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 A13; :: thesis: verum