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 n = len x; :: thesis: for x being FinSequence st x in dom f holds
n = len x
let y be FinSequence; :: thesis: ( y in dom f implies n = len y )
assume y in dom f ; :: thesis: n = len y
then dom x = dom y by A1, CARD_3:def 10;
hence n = len y by FINSEQ_3:31; :: thesis: verum

end;

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