let v1, v2 be Element of X; :: thesis: ( ex f being Function of NAT ,the carrier of X st
( v1 = f . n & f . 0 = x & ( for j being Element of NAT st j < n holds
f . (j + 1) = (f . j) \ y ) ) & ex f being Function of NAT ,the carrier of X st
( v2 = f . n & f . 0 = x & ( for j being Element of NAT st j < n holds
f . (j + 1) = (f . j) \ y ) ) implies v1 = v2 )
given f being Function of NAT ,the carrier of X such that A19: v1 = f . n and
A20: f . 0 = x and
A21: for j being Element of NAT st j < n holds
f . (j + 1) = (f . j) \ y ; :: thesis: ( for f being Function of NAT ,the carrier of X holds
( not v2 = f . n or not f . 0 = x or ex j being Element of NAT st
( j < n & not f . (j + 1) = (f . j) \ y ) ) or v1 = v2 )
given f9 being Function of NAT ,the carrier of X such that A22: v2 = f9 . n and
A23: f9 . 0 = x and
A24: for j being Element of NAT st j < n holds
f9 . (j + 1) = (f9 . j) \ y ; :: thesis: v1 = v2
defpred S₁[ Nat] means ( $1 <= n implies f . $1 = f9 . $1 );

now

let k be Element of NAT ; :: thesis: ( ( k <= n implies f . k = f9 . k ) & k + 1 <= n implies f . (k + 1) = f9 . (k + 1) )
assume A25: ( k <= n implies f . k = f9 . k ) ; :: thesis: ( k + 1 <= n implies f . (k + 1) = f9 . (k + 1) )
assume k + 1 <= n ; :: thesis: f . (k + 1) = f9 . (k + 1)
then A26: k < n by NAT_1:13;
then f . (k + 1) = (f . k) \ y by A21;
hence f . (k + 1) = f9 . (k + 1) by A24, A25, A26; :: thesis: verum

end;

then A27: for k being Element of NAT st S₁[k] holds
S₁[k + 1] ;
A28: S₁[ 0 ] by A20, A23;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A28, A27);
hence v1 = v2 by A19, A22; :: thesis: verum