defpred S1[ Element of BOOLEAN * , object ] means ex x0 being Tuple of len $1, BOOLEAN st
( $1 = x0 & $2 = Absval x0 );
A1: for x being Element of BOOLEAN * ex y being Element of NAT st S1[x,y]
proof
let x be Element of BOOLEAN * ; :: thesis: ex y being Element of NAT st S1[x,y]
x is Element of (len x) -tuples_on BOOLEAN by FINSEQ_2:92;
then reconsider x0 = x as Tuple of len x, BOOLEAN ;
reconsider n = Absval x0 as Element of NAT ;
take n ; :: thesis: S1[x,n]
thus ex x0 being Tuple of len x, BOOLEAN st
( x = x0 & n = Absval x0 ) ; :: thesis: verum
end;
consider f being Function of (BOOLEAN *),NAT such that
A2: for x being Element of BOOLEAN * holds S1[x,f . x] from FUNCT_2:sch 3(A1);
 take f ; :: thesis: for x being Element of BOOLEAN * ex x0 being Tuple of len x, BOOLEAN st
( x = x0 & f . x = Absval x0 )
thus for x being Element of BOOLEAN * ex x0 being Tuple of len x, BOOLEAN st
( x = x0 & f . x = Absval x0 ) by A2; :: thesis: verum