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 S₁[ 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 S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume that
A5: S₁[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: S₁[ 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 S₁[n] from NAT_1:sch 2(A9, A4);
hence Product ((i -' j) |-> rr) = (Product (i |-> rr)) / (Product (j |-> rr)) by A2; :: thesis: verum