reconsider mm = r as Element of INT by INT_1:def 2;
take r ; :: thesis: ex f being FinSequence of INT st
( f = x `3_3 & r = f /. 1 )
take <*mm*> ; :: thesis: ( <*mm*> = x `3_3 & r = <*mm*> /. 1 )
thus ( <*mm*> = x `3_3 & r = <*mm*> /. 1 ) by A1, FINSEQ_4:16; :: thesis: verum