let R be Relation; :: thesis: ( R is empty implies R is with_the_same_arity )
assume A1: R is empty ; :: thesis: R is with_the_same_arity
let f, g be Function; :: according to COMPUT_1:def 6 :: thesis: ( f in rng R & g in rng R implies ( ( not f is empty or g is empty or dom g = {{} } ) & ( not f is empty & not g is empty implies ex n being Element of NAT ex X being non empty set st
( dom f c= n -tuples_on X & dom g c= n -tuples_on X ) ) ) )
thus ( f in rng R & g in rng R implies ( ( not f is empty or g is empty or dom g = {{} } ) & ( not f is empty & not g is empty implies ex n being Element of NAT ex X being non empty set st
( dom f c= n -tuples_on X & dom g c= n -tuples_on X ) ) ) ) by A1; :: thesis: verum