let h, g be Function; :: according to COMPUT_1:def 6 :: 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 A1: ( h in rng <*f*> & 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 ) ) )
rng <*f*> = {f} by FINSEQ_1:56;
then A2: ( h = f & g = f ) by A1, TARSKI:def 1;
hence ( not h is empty or g is empty or dom g = {{} } ) ; :: 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 ( not h is empty & 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 i = arity f; :: thesis: ex X being non empty set st
( dom h c= i -tuples_on X & dom g c= i -tuples_on X )
take NAT ; :: thesis: ( dom h c= i -tuples_on NAT & dom g c= i -tuples_on NAT )
thus ( dom h c= i -tuples_on NAT & dom g c= i -tuples_on NAT ) by A2, Th24; :: thesis: verum