let v1, v2 be Element of X; ( 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
; ( 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
; v1 = v2
defpred S1[ Nat] means ( $1 <= n implies f . $1 = f9 . $1 );
now 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;
( ( 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 )
;
( k + 1 <= n implies f . (k + 1) = f9 . (k + 1) )assume
k + 1
<= n
;
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;
verum end;
then A28:
for k being Nat st S1[k] holds
S1[k + 1]
;
A29:
S1[ 0 ]
by A21, A24;
for k being Nat holds S1[k]
from NAT_1:sch 2(A29, A28);
hence
v1 = v2
by A20, A23; verum