defpred S1[ 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: S1[ 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 S1[k] holds
S1[k + 1] by Lm12;
for n being Nat holds S1[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