let m be Nat; :: thesis: for x being Tuple of 1, INT st x /. 1 = m holds
x = <*m*>
let x be Tuple of 1, INT ; :: thesis: ( x /. 1 = m implies x = <*m*> )
assume A1: x /. 1 = m ; :: thesis: x = <*m*>
A2: len x = 1 by CARD_1:def 7;
then x /. 1 = x . 1 by FINSEQ_4:15;
hence x = <*m*> by A1, A2, FINSEQ_1:40; :: thesis: verum