let x be Function of REAL,REAL; :: thesis: for n being Nat
for a being Real st (@ (@ x)) . a > 0 holds
(@ ((@ x) |^ n)) . a = ((@ (@ x)) . a) |^ n
let n be Nat; :: thesis: for a being Real st (@ (@ x)) . a > 0 holds
(@ ((@ x) |^ n)) . a = ((@ (@ x)) . a) |^ n
let a be Real; :: thesis: ( (@ (@ x)) . a > 0 implies (@ ((@ x) |^ n)) . a = ((@ (@ x)) . a) |^ n )
assume A1: (@ (@ x)) . a > 0 ; :: thesis: (@ ((@ x) |^ n)) . a = ((@ (@ x)) . a) |^ n
defpred S₁[ Nat] means (@ ((@ x) |^ $1)) . a = ((@ (@ x)) . a) |^ $1;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
@ ((@ x) |^ (n + 1)) = ((@ x) |^ n) * (@ x) by Th20
.= (@ ((@ x) |^ n)) (#) (@ (@ x)) by Th13 ;
then (@ ((@ x) |^ (n + 1))) . a = (((@ (@ x)) . a) to_power n) * (((@ (@ x)) . a) to_power 1) by A3, VALUED_1:5
.= ((@ (@ x)) . a) to_power (n + 1) by A1, POWER:27
.= ((@ (@ x)) . a) |^ (n + 1) ;
hence S₁[n + 1] ; :: thesis: verum

end;

A4: S₁[ 0 ]

proof

A5: ((@ (@ x)) . a) |^ 0 = ((@ (@ x)) . a) to_power 0
.= 1 by POWER:24 ;
@ ((@ x) |^ 0) = REAL --> 1 by Lm5;
hence S₁[ 0 ] by A5, XREAL_0:def 1, FUNCOP_1:7; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A2);
hence (@ ((@ x) |^ n)) . a = ((@ (@ x)) . a) |^ n ; :: thesis: verum