thus ex IT, n being Nat ex y being Tuple of n, BOOLEAN st
( y = x & IT = Absval y ) :: thesis: verum

proof

reconsider n = len x as Nat ;
reconsider y = x as Tuple of n, BOOLEAN by CARD_1:def 7;
take IT = Absval y; :: thesis: ex n being Nat ex y being Tuple of n, BOOLEAN st
( y = x & IT = Absval y )
thus ex n being Nat ex y being Tuple of n, BOOLEAN st
( y = x & IT = Absval y ) ; :: thesis: verum

end;