defpred S₁[ Element of NAT , object ] means $2 = (LenBSeq $1) -BinarySequence $1;
A1: for x being Element of NAT ex y being Element of BOOLEAN * st S₁[x,y]

proof

let x be Element of NAT ; :: thesis: ex y being Element of BOOLEAN * st S₁[x,y]
set y = (LenBSeq x) -BinarySequence x;
reconsider y = (LenBSeq x) -BinarySequence x as Element of BOOLEAN * by FINSEQ_1:def 11;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] ; :: thesis: verum

end;

consider f being Function of NAT,(BOOLEAN *) such that
A2: for x being Element of NAT holds S₁[x,f . x] from FUNCT_2:sch 3(A1);
take f ; :: thesis: for x being Element of NAT holds f . x = (LenBSeq x) -BinarySequence x
thus for x being Element of NAT holds f . x = (LenBSeq x) -BinarySequence x by A2; :: thesis: verum