let v1, v2 be Element of X; :: thesis: ( ex f being sequence of the carrier of X st
( v1 = f . n & f . 0 = x & ( for j being Nat st j < n holds
f . (j + 1) = (f . j) \ y ) ) & ex f being sequence of the carrier of X st
( v2 = f . n & f . 0 = x & ( for j being Nat st j < n holds
f . (j + 1) = (f . j) \ y ) ) implies v1 = v2 )
given f being sequence of the carrier of X such that A20: v1 = f . n and
A21: f . 0 = x and
A22: for j being Nat st j < n holds
f . (j + 1) = (f . j) \ y ; :: thesis: ( for f being sequence of the carrier of X holds
( not v2 = f . n or not f . 0 = x or ex j being Nat st
( j < n & not f . (j + 1) = (f . j) \ y ) ) or v1 = v2 )
given f9 being sequence of the carrier of X such that A23: v2 = f9 . n and
A24: f9 . 0 = x and
A25: for j being 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 :: thesis: for k being Nat st ( k <= n implies f . k = f9 . k ) & k + 1 <= n holds
f . (k + 1) = f9 . (k + 1)

let k be Nat; :: thesis: ( ( k <= n implies f . k = f9 . k ) & k + 1 <= n implies f . (k + 1) = f9 . (k + 1) )
assume A26: ( 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 A27: k < n by NAT_1:13;
then f . (k + 1) = (f . k) \ y by A22;
hence f . (k + 1) = f9 . (k + 1) by A25, A26, A27; :: thesis: verum

end;

then A28: for k being Nat st S₁[k] holds
S₁[k + 1] ;
A29: S₁[ 0 ] by A21, A24;
for k being Nat holds S₁[k] from NAT_1:sch 2(A29, A28);
hence v1 = v2 by A20, A23; :: thesis: verum