let h, g be Function; :: according to COMPUT_1:def 3 :: thesis: ( h in rng <*f*> & g in rng <*f*> implies ( ( not h is empty or g is empty or dom g = {{}} ) & ( not h is empty & not g is empty implies ex n being Element of NAT ex X being non empty set st
( dom h c= n -tuples_on X & dom g c= n -tuples_on X ) ) ) )
assume that
A1: h in rng <*f*> and
A2: g in rng <*f*> ; :: thesis: ( ( not h is empty or g is empty or dom g = {{}} ) & ( not h is empty & not g is empty implies ex n being Element of NAT ex X being non empty set st
( dom h c= n -tuples_on X & dom g c= n -tuples_on X ) ) )
A3: rng <*f*> = {f} by FINSEQ_1:39;
then A4: h = f by A1, TARSKI:def 1;
hence ( not h is empty or g is empty or dom g = {{}} ) by A2, A3, TARSKI:def 1; :: thesis: ( not h is empty & not g is empty implies ex n being Element of NAT ex X being non empty set st
( dom h c= n -tuples_on X & dom g c= n -tuples_on X ) )
assume that
not h is empty and
not g is empty ; :: thesis: ex n being Element of NAT ex X being non empty set st
( dom h c= n -tuples_on X & dom g c= n -tuples_on X )
take arity f ; :: thesis: ex X being non empty set st
( dom h c= (arity f) -tuples_on X & dom g c= (arity f) -tuples_on X )
take NAT ; :: thesis: ( dom h c= (arity f) -tuples_on NAT & dom g c= (arity f) -tuples_on NAT )
g = f by A2, A3, TARSKI:def 1;
hence ( dom h c= (arity f) -tuples_on NAT & dom g c= (arity f) -tuples_on NAT ) by A4, Th20; :: thesis: verum