defpred S₁[ Element of NAT ] means for r being Real st r > 0 holds
Product ($1 |-> r) = r to_power $1;
A1: S₁[ 0 ]

proof

let r be Real; :: thesis: ( r > 0 implies Product (0 |-> r) = r to_power 0 )
assume r > 0 ; :: thesis: Product (0 |-> r) = r to_power 0
Product (0 |-> r) = 1 by FINSEQ_2:72, RVSUM_1:124;
hence Product (0 |-> r) = r to_power 0 by POWER:29; :: thesis: verum

end;

A2: 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 A3: S₁[n] ; :: thesis: S₁[n + 1]

now

let r be Real; :: thesis: ( r > 0 implies Product ((n + 1) |-> r) = r to_power (n + 1) )
assume A4: r > 0 ; :: thesis: Product ((n + 1) |-> r) = r to_power (n + 1)
Product ((n + 1) |-> r) = Product ((n |-> r) ^ <*r*>) by FINSEQ_2:74
.= (Product (n |-> r)) * r by RVSUM_1:126
.= (r to_power n) * r by A3, A4
.= (r to_power n) * (r to_power 1) by POWER:30 ;
hence Product ((n + 1) |-> r) = r to_power (n + 1) by A4, POWER:32; :: thesis: verum

end;

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

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A2);
hence for n being Element of NAT
for r being Real st r > 0 holds
Product (n |-> r) = r to_power n ; :: thesis: verum