set S = i -tuples_on D;
let f, g be Function; :: according to CARD_3:def 10 :: thesis: ( not f in i -tuples_on D or not g in i -tuples_on D or dom f = dom g )
assume A1: ( f in i -tuples_on D & g in i -tuples_on D ) ; :: thesis: dom f = dom g
i -tuples_on D = { s where s is Element of D * : len s = i } by FINSEQ_2:def 4;
then ( ex s being Element of D * st
( f = s & len s = i ) & ex s being Element of D * st
( g = s & len s = i ) ) by A1;
hence dom f = dom g by FINSEQ_3:31; :: thesis: verum