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₁[ Nat] means ( $1 in dom ft implies (ft . $1) * (Product (Del (ft,$1))) = Product ft );
A1: for a being Nat st S₁[a] holds
S₁[a + 1]

proof

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

now :: thesis: S₁[a + 1]

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

suppose A2: a = 0 ; :: thesis: S₁[a + 1]

thus S₁[a + 1] :: thesis: verum

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;

end;

suppose ( a > 0 & a < len ft ) ; :: thesis: S₁[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₁[a + 1] by A6, RVSUM_1:97; :: thesis: verum

end;

suppose a >= len ft ; :: thesis: S₁[a + 1]

then len ft < a + 1 by NAT_1:13;
hence S₁[a + 1] by FINSEQ_3:25; :: thesis: verum

end;

end;

end;

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

end;

A7: S₁[ 0 ] by FINSEQ_3:25;
for a being Nat holds S₁[a] from NAT_1:sch 2(A7, A1);
hence ( a in dom ft implies (Product (Del (ft,a))) * (ft . a) = Product ft ) ; :: thesis: verum