defpred S₁[ Nat] means for p being FinSequence
for A being set st len p = $1 holds
for n being Nat st n in dom p holds
for B being finite set holds
( not B = { k where k is Element of NAT : ( k in dom p & k <= n & p . k in A ) } or p . n in A or (p - A) . (n - (card B)) = p . n );
A1: S₁[ 0 ]

proof

let p be FinSequence; :: thesis: for A being set st len p = 0 holds
for n being Nat st n in dom p holds
for B being finite set holds
( not B = { k where k is Element of NAT : ( k in dom p & k <= n & p . k in A ) } or p . n in A or (p - A) . (n - (card B)) = p . n )
let A be set ; :: thesis: ( len p = 0 implies for n being Nat st n in dom p holds
for B being finite set holds
( not B = { k where k is Element of NAT : ( k in dom p & k <= n & p . k in A ) } or p . n in A or (p - A) . (n - (card B)) = p . n ) )
assume len p = 0 ; :: thesis: for n being Nat st n in dom p holds
for B being finite set holds
( not B = { k where k is Element of NAT : ( k in dom p & k <= n & p . k in A ) } or p . n in A or (p - A) . (n - (card B)) = p . n )
then p = {} ;
hence for n being Nat st n in dom p holds
for B being finite set holds
( not B = { k where k is Element of NAT : ( k in dom p & k <= n & p . k in A ) } or p . n in A or (p - A) . (n - (card B)) = p . n ) ; :: thesis: verum

end;

A2: for k being Nat st S₁[k] holds
S₁[k + 1] by Lm12;
for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
hence for l being Nat
for p being FinSequence
for A being set st len p = l holds
for n being Nat st n in dom p holds
for B being finite set holds
( not B = { k where k is Element of NAT : ( k in dom p & k <= n & p . k in A ) } or p . n in A or (p - A) . (n - (card B)) = p . n ) ; :: thesis: verum