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 proj1 f = proj1 g )
assume that
A1: f in i -tuples_on D and
A2: g in i -tuples_on D ; :: thesis: proj1 f = proj1 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 proj1 f = proj1 g by A3, Th31; :: thesis: verum