let L be non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive doubleLoopStr ; :: thesis: for n being Element of NAT holds (1_. L) `^ n = 1_. L
defpred S<sub>1</sub>[ Element of NAT ] means (1_. L) `^ $1 = 1_. L;

A1: now

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then (1_. L) `^ (n + 1) = (1_. L) *' (1_. L) by Th20
.= 1_. L by POLYNOM3:36 ;
hence S₁[n + 1] ; :: thesis: verum

end;

A2: S₁[ 0 ] by Th16;
thus for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A1); :: thesis: verum