defpred S₁[ Nat] means for A, B being decreasing Ordinal-Sequence st len A = $1 & rng A = rng B holds
A = B;
A1: S₁[ 0 ]

proof

let A, B be decreasing Ordinal-Sequence; :: thesis: ( len A = 0 & rng A = rng B implies A = B )
assume A2: ( len A = 0 & rng A = rng B ) ; :: thesis: A = B
then A is empty ;
hence A = B by A2; :: thesis: verum

end;

A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
let A, B be decreasing Ordinal-Sequence; :: thesis: ( len A = n + 1 & rng A = rng B implies A = B )
assume A5: ( len A = n + 1 & rng A = rng B ) ; :: thesis: A = B
dom A = card (dom A)
.= card (rng B) by A5, CARD_1:70
.= card (dom B) by CARD_1:70
.= dom B ;
then A6: len B = n + 1 by A5;
set A0 = A | n;
set B0 = B | n;
( rng (A | n) = (rng A) \ {(A . n)} & rng (B | n) = (rng B) \ {(B . n)} ) by A5, A6, Lm6;
then A7: rng (A | n) = rng (B | n) by A5, Lm7;
A8: len (A | n) = (dom A) /\ n by RELAT_1:61
.= (succ n) /\ n by A5, Lm5
.= n by Th1 ;
thus A = (A | n) ^ <%(A . n)%> by A5, AFINSQ_1:56
.= (B | n) ^ <%(A . n)%> by A4, A7, A8
.= (B | n) ^ <%(B . n)%> by A5, Lm7
.= B by A6, AFINSQ_1:56 ; :: thesis: verum

end;

A9: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A3);
let A, B be decreasing Ordinal-Sequence; :: thesis: ( rng A = rng B implies A = B )
assume A10: rng A = rng B ; :: thesis: A = B
len A is Nat ;
hence A = B by A9, A10; :: thesis: verum