thus ( ex x being FinSequence st x in dom f implies ex n being Nat st
for x being FinSequence st x in dom f holds
n = len x ) :: thesis: ( ( for x being FinSequence holds not x in dom f ) implies ex b₁ being Nat st b₁ = 0 )

proof

given x being FinSequence such that A1: x in dom f ; :: thesis: ex n being Nat st
for x being FinSequence st x in dom f holds
n = len x
take len x ; :: thesis: for x being FinSequence st x in dom f holds
len x = len x
let y be FinSequence; :: thesis: ( y in dom f implies len x = len y )
assume y in dom f ; :: thesis: len x = len y
then dom x = dom y by A1, CARD_3:def 10;
hence len x = len y by FINSEQ_3:29; :: thesis: verum

end;

thus ( ( for x being FinSequence holds not x in dom f ) implies ex b₁ being Nat st b₁ = 0 ) ; :: thesis: verum