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 FINSEQ_1:def 18;
then x /. 1 = x . 1 by FINSEQ_4:24;
hence x = <*m*> by A1, A2, FINSEQ_1:57; :: thesis: verum