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

proof

let n be non zero Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume 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) |^ n)) . a) * ((@ (@ x)) . a) by VALUED_1:5
.= 0 by A1 ;
hence S₁[n + 1] ; :: thesis: verum

end;

A3: S₁[1] by A1, BINOM:8;
for n being non zero Nat holds S₁[n] from NAT_1:sch 10(A3, A2);
hence (@ ((@ x) |^ n)) . a = 0 ; :: thesis: verum