let a be Nat; :: thesis: for ft being FinSequence of REAL st a in dom ft holds

(Product (Del (ft,a))) * (ft . a) = Product ft

let ft be FinSequence of REAL ; :: thesis: ( a in dom ft implies (Product (Del (ft,a))) * (ft . a) = Product ft )

defpred S_{1}[ Nat] means ( $1 in dom ft implies (ft . $1) * (Product (Del (ft,$1))) = Product ft );

A1: for a being Nat st S_{1}[a] holds

S_{1}[a + 1]
_{1}[ 0 ]
by FINSEQ_3:25;

for a being Nat holds S_{1}[a]
from NAT_1:sch 2(A7, A1);

hence ( a in dom ft implies (Product (Del (ft,a))) * (ft . a) = Product ft ) ; :: thesis: verum

(Product (Del (ft,a))) * (ft . a) = Product ft

let ft be FinSequence of REAL ; :: thesis: ( a in dom ft implies (Product (Del (ft,a))) * (ft . a) = Product ft )

defpred S

A1: for a being Nat st S

S

proof

A7:
S
let a be Nat; :: thesis: ( S_{1}[a] implies S_{1}[a + 1] )

assume S_{1}[a]
; :: thesis: S_{1}[a + 1]

_{1}[a + 1]
; :: thesis: verum

end;assume S

now :: thesis: S_{1}[a + 1]end;

hence
Sper cases
( a = 0 or ( a > 0 & a < len ft ) or a >= len ft )
;

end;

suppose A2:
a = 0
; :: thesis: S_{1}[a + 1]

thus
S_{1}[a + 1]
:: thesis: verum

end;proof

assume
a + 1 in dom ft
; :: thesis: (ft . (a + 1)) * (Product (Del (ft,(a + 1)))) = Product ft

then a + 1 <= len ft by FINSEQ_3:25;

then <*(ft . 1)*> ^ (Del (ft,1)) = ft by A2, Lm7;

then Product ft = (Product <*(ft . 1)*>) * (Product (Del (ft,1))) by RVSUM_1:97

.= (ft . 1) * (Product (Del (ft,1))) ;

hence (ft . (a + 1)) * (Product (Del (ft,(a + 1)))) = Product ft by A2; :: thesis: verum

end;then a + 1 <= len ft by FINSEQ_3:25;

then <*(ft . 1)*> ^ (Del (ft,1)) = ft by A2, Lm7;

then Product ft = (Product <*(ft . 1)*>) * (Product (Del (ft,1))) by RVSUM_1:97

.= (ft . 1) * (Product (Del (ft,1))) ;

hence (ft . (a + 1)) * (Product (Del (ft,(a + 1)))) = Product ft by A2; :: thesis: verum

suppose
( a > 0 & a < len ft )
; :: thesis: S_{1}[a + 1]

then
( a + 1 >= 1 & a + 1 <= len ft )
by NAT_1:11, NAT_1:13;

then A3: a + 1 in dom ft by FINSEQ_3:25;

then consider fs1, fs2 being FinSequence such that

A4: ft = (fs1 ^ <*(ft . (a + 1))*>) ^ fs2 and

A5: len fs1 = (a + 1) - 1 and

len fs2 = (len ft) - (a + 1) by Lm5;

A6: Del (ft,(a + 1)) = fs1 ^ fs2 by A3, A4, A5, Lm6;

reconsider fs2 = fs2 as FinSequence of REAL by A4, FINSEQ_1:36;

reconsider fs1 = fs1 as FinSequence of REAL by A6, FINSEQ_1:36;

Product ft = (Product (fs1 ^ <*(ft . (a + 1))*>)) * (Product fs2) by A4, RVSUM_1:97

.= ((Product fs1) * (Product <*(ft . (a + 1))*>)) * (Product fs2) by RVSUM_1:97

.= ((ft . (a + 1)) * (Product fs1)) * (Product fs2)

.= (ft . (a + 1)) * ((Product fs1) * (Product fs2)) ;

hence S_{1}[a + 1]
by A6, RVSUM_1:97; :: thesis: verum

end;then A3: a + 1 in dom ft by FINSEQ_3:25;

then consider fs1, fs2 being FinSequence such that

A4: ft = (fs1 ^ <*(ft . (a + 1))*>) ^ fs2 and

A5: len fs1 = (a + 1) - 1 and

len fs2 = (len ft) - (a + 1) by Lm5;

A6: Del (ft,(a + 1)) = fs1 ^ fs2 by A3, A4, A5, Lm6;

reconsider fs2 = fs2 as FinSequence of REAL by A4, FINSEQ_1:36;

reconsider fs1 = fs1 as FinSequence of REAL by A6, FINSEQ_1:36;

Product ft = (Product (fs1 ^ <*(ft . (a + 1))*>)) * (Product fs2) by A4, RVSUM_1:97

.= ((Product fs1) * (Product <*(ft . (a + 1))*>)) * (Product fs2) by RVSUM_1:97

.= ((ft . (a + 1)) * (Product fs1)) * (Product fs2)

.= (ft . (a + 1)) * ((Product fs1) * (Product fs2)) ;

hence S

for a being Nat holds S

hence ( a in dom ft implies (Product (Del (ft,a))) * (ft . a) = Product ft ) ; :: thesis: verum