set X = i -tuples_on NAT ;
set g = f | (i -tuples_on NAT );
A1: dom (f | (i -tuples_on NAT )) c= i -tuples_on NAT by RELAT_1:87;
let x, y be FinSequence; :: according to UNIALG_1:def 1 :: thesis: ( x in dom (f | (i -tuples_on NAT )) & y in dom (f | (i -tuples_on NAT )) implies len x = len y )
assume ( x in dom (f | (i -tuples_on NAT )) & y in dom (f | (i -tuples_on NAT )) ) ; :: thesis: len x = len y
then ( len x = i & len y = i ) by A1, FINSEQ_1:def 18;
hence len x = len y ; :: thesis: verum