let E be set ; :: thesis: for n being Nat holds {(<%> E)} |^ n = {(<%> E)}
let n be Nat; :: thesis: {(<%> E)} |^ n = {(<%> E)}
defpred S₁[ Nat] means {(<%> E)} |^ $1 = {(<%> E)};

A1: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
{(<%> E)} |^ (n + 1) = ({(<%> E)} |^ n) ^^ {(<%> E)} by Th23
.= {(<%> E)} by A2, Th13 ;
hence S₁[n + 1] ; :: thesis: verum

end;

A3: S₁[ 0 ] by Th24;
for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A1);
hence {(<%> E)} |^ n = {(<%> E)} ; :: thesis: verum