defpred S₁[ Nat] means f |^ $1 = ZeroMap (V,V);
A1: ex n being Nat st S₁[n] by Th13;
consider n being Nat such that
A2: ( S₁[n] & ( for k being Nat st S₁[k] holds
n <= k ) ) from NAT_1:sch 5(A1);
take n ; :: thesis: ( f |^ n = ZeroMap (V,V) & ( for k being Nat st f |^ k = ZeroMap (V,V) holds
n <= k ) )
thus ( f |^ n = ZeroMap (V,V) & ( for k being Nat st f |^ k = ZeroMap (V,V) holds
n <= k ) ) by A2; :: thesis: verum