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 that
A1: f in i -tuples_on D and
A2: g in i -tuples_on D ; :: thesis: dom f = dom g
A3: ex s being Element of D * st
( f = s & len s = i ) by A1;
ex s being Element of D * st
( g = s & len s = i ) by A2;
hence dom f = dom g by A3, Th27; :: thesis: verum