let X, Y be RealLinearSpace; :: thesis: for L being LinearOperator of X,Y
for F being FinSequence of X holds L . (Sum F) = Sum (L * F)
let L be LinearOperator of X,Y; :: thesis: for F being FinSequence of X holds L . (Sum F) = Sum (L * F)
let F be FinSequence of X; :: thesis: L . (Sum F) = Sum (L * F)
defpred S₁[ set ] means for H being FinSequence of X st len H = $1 holds
L . (Sum H) = Sum (L * H);
A1: dom F = Seg (len F) by FINSEQ_1:def 3;
A2: S₁[ 0 ]

proof

let H be FinSequence of X; :: thesis: ( len H = 0 implies L . (Sum H) = Sum (L * H) )
assume A3: len H = 0 ; :: thesis: L . (Sum H) = Sum (L * H)
then H = {} ;
then A4: L * H = <*> the carrier of Y ;
A5: L is additive ;
L . (0. X) = L . ((0. X) + (0. X))
.= (L . (0. X)) + (L . (0. X)) by A5 ;
then L . (0. X) = 0. Y by RLVECT_1:9;
hence L . (Sum H) = 0. Y by A3, RLVECT_1:75
.= Sum (L * H) by A4, RLVECT_1:43 ;
:: thesis: verum

end;

A6: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A7: for H being FinSequence of X st len H = n holds
L . (Sum H) = Sum (L * H) ; :: thesis: S₁[n + 1]
let H be FinSequence of X; :: thesis: ( len H = n + 1 implies L . (Sum H) = Sum (L * H) )
assume A8: len H = n + 1 ; :: thesis: L . (Sum H) = Sum (L * H)
reconsider p = H | (Seg n) as FinSequence of the carrier of X by FINSEQ_1:18;
A9: n <= n + 1 by NAT_1:12;
then A10: len p = n by A8, FINSEQ_1:17;
A11: dom p = Seg n by A8, A9, FINSEQ_1:17;
1 <= n + 1 by NAT_1:11;
then A12: n + 1 in dom H by A8, FINSEQ_3:25;
then reconsider v1 = H . (n + 1) as VECTOR of X by FUNCT_1:102;
A13: L . v1 = (L * H) . (n + 1) by A12, FUNCT_1:13;
A14: dom L = the carrier of X by FUNCT_2:def 1;
rng H c= the carrier of X ;
then dom (L * H) = dom H by A14, RELAT_1:27;
then A15: dom (L * H) = Seg (len H) by FINSEQ_1:def 3
.= Seg (n + 1) by A8 ;
then A16: len (L * H) = n + 1 by FINSEQ_1:def 3;
rng p c= the carrier of X ;
then A17: dom (L * p) = dom p by A14, RELAT_1:27;
reconsider Lp = L * p as FinSequence ;
A18: n is Element of NAT by ORDINAL1:def 12;
A19: dom (L * p) = Seg (len p) by A17, FINSEQ_1:def 3
.= Seg n by A8, A9, FINSEQ_1:17 ;
then A20: len (L * p) = n by A18, FINSEQ_1:def 3;
A21: Seg n c= Seg (n + 1) by NAT_1:12, FINSEQ_1:5;
for i being object st i in dom ((L * H) | (dom (L * p))) holds
((L * H) | (dom (L * p))) . i = (L * p) . i

proof

let i be object ; :: thesis: ( i in dom ((L * H) | (dom (L * p))) implies ((L * H) | (dom (L * p))) . i = (L * p) . i )
assume A22: i in dom ((L * H) | (dom (L * p))) ; :: thesis: ((L * H) | (dom (L * p))) . i = (L * p) . i
then A23: i in (dom (L * H)) /\ (dom (L * p)) by RELAT_1:61;
then A24: ( i in dom (L * H) & i in dom (L * p) ) by XBOOLE_0:def 4;
A25: i in dom p by A11, A19, A23, XBOOLE_0:def 4;
thus ((L * H) | (dom (L * p))) . i = (L * H) . i by A22, FUNCT_1:47
.= L . (H . i) by A24, FUNCT_1:12
.= L . (p . i) by A25, FUNCT_1:47
.= (L * p) . i by A24, FUNCT_1:12 ; :: thesis: verum

end;

then A26: (L * H) | (dom (L * p)) = L * p by A15, A19, A21, FUNCT_1:2, RELAT_1:62;
A27: L is additive ;
thus L . (Sum H) = L . ((Sum p) + v1) by A8, A10, A11, RLVECT_1:38
.= (L . (Sum p)) + (L . v1) by A27
.= (Sum (L * p)) + (L . v1) by A7, A10
.= Sum (L * H) by A13, A16, A20, A26, RLVECT_1:38 ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A6);
hence L . (Sum F) = Sum (L * F) by A1; :: thesis: verum