let r be Real; :: thesis: for j, i being Element of NAT st r <> 0 & j <= i holds
Product ((i -' j) |-> r) = (Product (i |-> r)) / (Product (j |-> r))
let j, i be Element of NAT ; :: thesis: ( r <> 0 & j <= i implies Product ((i -' j) |-> r) = (Product (i |-> r)) / (Product (j |-> r)) )
assume that
A1: r <> 0 and
A2: j <= i ; :: thesis: Product ((i -' j) |-> r) = (Product (i |-> r)) / (Product (j |-> r))
defpred S₁[ Element of NAT ] means ( j <= $1 implies Product (($1 -' j) |-> r) = (Product ($1 |-> r)) / (Product (j |-> r)) );
A3: Product (j |-> r) <> 0 by A1, Th13;
A4: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume that
A5: S₁[n] and
A6: j <= n + 1 ; :: thesis: Product (((n + 1) -' j) |-> r) = (Product ((n + 1) |-> r)) / (Product (j |-> r))

per cases ( j <= n or j = n + 1 ) by A6, NAT_1:8;

suppose A7: j <= n ; :: thesis: Product (((n + 1) -' j) |-> r) = (Product ((n + 1) |-> r)) / (Product (j |-> r))

Product (((n -' j) + 1) |-> r) = (Product ((n -' j) |-> r)) * (Product (1 |-> r)) by RVSUM_1:104
.= ((Product (n |-> r)) / (Product (j |-> r))) * r by A5, A7, Th10
.= ((Product (n |-> r)) * r) / (Product (j |-> r)) by XCMPLX_1:74
.= (Product ((n + 1) |-> r)) / (Product (j |-> r)) by Th12 ;
hence Product (((n + 1) -' j) |-> r) = (Product ((n + 1) |-> r)) / (Product (j |-> r)) by A7, NAT_D:38; :: thesis: verum

end;

suppose A8: j = n + 1 ; :: thesis: Product (((n + 1) -' j) |-> r) = (Product ((n + 1) |-> r)) / (Product (j |-> r))

hence Product (((n + 1) -' j) |-> r) = Product (0 |-> r) by XREAL_1:232
.= 1 by RVSUM_1:94
.= (Product ((n + 1) |-> r)) / (Product (j |-> r)) by A3, A8, XCMPLX_1:60 ;
:: thesis: verum

end;

end;

end;

A9: S₁[ 0 ]

proof

assume A10: j <= 0 ; :: thesis: Product ((0 -' j) |-> r) = (Product (0 |-> r)) / (Product (j |-> r))
then j = 0 by NAT_1:3;
hence Product ((0 -' j) |-> r) = (Product (0 |-> r)) / (Product (<*> REAL)) by NAT_D:40, RVSUM_1:94
.= (Product (0 |-> r)) / (Product (j |-> r)) by A10, NAT_1:3 ;
:: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A9, A4);
hence Product ((i -' j) |-> r) = (Product (i |-> r)) / (Product (j |-> r)) by A2; :: thesis: verum