let N1, N2 be Nat; :: thesis: ( ex n being Nat ex y being Tuple of n, BOOLEAN st
( y = x & N1 = Absval y ) & ex n being Nat ex y being Tuple of n, BOOLEAN st
( y = x & N2 = Absval y ) implies N1 = N2 )
thus ( ex n being Nat ex y being Tuple of n, BOOLEAN st
( y = x & N1 = Absval y ) & ex n being Nat ex y being Tuple of n, BOOLEAN st
( y = x & N2 = Absval y ) implies N1 = N2 ) :: thesis: verum

proof

assume that
A2: ex n being Nat ex y being Tuple of n, BOOLEAN st
( y = x & N1 = Absval y ) and
A3: ex n being Nat ex y being Tuple of n, BOOLEAN st
( y = x & N2 = Absval y ) ; :: thesis: N1 = N2
consider n1 being Nat, y1 being Tuple of n1, BOOLEAN such that
A4: ( y1 = x & N1 = Absval y1 ) by A2;
consider n2 being Nat, y2 being Tuple of n2, BOOLEAN such that
A5: ( y2 = x & N2 = Absval y2 ) by A3;
n1 = len y1 by CARD_1:def 7
.= n2 by CARD_1:def 7, A4, A5 ;
hence N1 = N2 by A4, A5; :: thesis: verum

end;