let rr be Real; :: thesis: for i, j being Nat st rr <> 0 & j <= i holds
Product ((i -' j) |-> rr) = (Product (i |-> rr)) / (Product (j |-> rr))
let i, j be Nat; :: thesis: ( rr <> 0 & j <= i implies Product ((i -' j) |-> rr) = (Product (i |-> rr)) / (Product (j |-> rr)) )
assume that
A1: rr <> 0 and
A2: j <= i ; :: thesis: Product ((i -' j) |-> rr) = (Product (i |-> rr)) / (Product (j |-> rr))
defpred S1[ Nat] means ( j <= $1 implies Product (($1 -' j) |-> rr) = (Product ($1 |-> rr)) / (Product (j |-> rr)) );
A3: Product (j |-> rr) <> 0 by A1, Th7;
A4: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume that
A5: S1[n] and
A6: j <= n + 1 ; :: thesis: Product (((n + 1) -' j) |-> rr) = (Product ((n + 1) |-> rr)) / (Product (j |-> rr))
per cases ( j <= n or j = n + 1 ) by A6, NAT_1:8;
suppose A7: j <= n ; :: thesis: Product (((n + 1) -' j) |-> rr) = (Product ((n + 1) |-> rr)) / (Product (j |-> rr))
Product (((n -' j) + 1) |-> rr) = (Product ((n -' j) |-> rr)) * (Product (1 |-> rr)) by RVSUM_1:104
.= ((Product (n |-> rr)) / (Product (j |-> rr))) * rr by A5, A7, Th4
.= ((Product (n |-> rr)) * rr) / (Product (j |-> rr)) by XCMPLX_1:74
.= (Product ((n + 1) |-> rr)) / (Product (j |-> rr)) by Th6 ;
hence Product (((n + 1) -' j) |-> rr) = (Product ((n + 1) |-> rr)) / (Product (j |-> rr)) by A7, NAT_D:38; :: thesis: verum
end;
suppose A8: j = n + 1 ; :: thesis: Product (((n + 1) -' j) |-> rr) = (Product ((n + 1) |-> rr)) / (Product (j |-> rr))
hence Product (((n + 1) -' j) |-> rr) = Product (0 |-> rr) by XREAL_1:232
.= 1 by RVSUM_1:94
.= (Product ((n + 1) |-> rr)) / (Product (j |-> rr)) by A3, A8, XCMPLX_1:60 ;
:: thesis: verum
end;
end;
end;
A9: S1[ 0 ]
proof
assume A10: j <= 0 ; :: thesis: Product ((0 -' j) |-> rr) = (Product (0 |-> rr)) / (Product (j |-> rr))
then j = 0 ;
hence Product ((0 -' j) |-> rr) = (Product (0 |-> rr)) / (Product (<*> REAL)) by NAT_D:40, RVSUM_1:94
.= (Product (0 |-> rr)) / (Product (j |-> rr)) by A10 ;
:: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A9, A4);
 hence Product ((i -' j) |-> rr) = (Product (i |-> rr)) / (Product (j |-> rr)) by A2; :: thesis: verum