let X be non empty set ; :: thesis: for F being Relation st rng F c= HFuncs X & ( for f, g being homogeneous Function st f in rng F & g in rng F holds
arity f = arity g ) holds
F is with_the_same_arity
let R be Relation; :: thesis: ( rng R c= HFuncs X & ( for f, g being homogeneous Function st f in rng R & g in rng R holds
arity f = arity g ) implies R is with_the_same_arity )
assume that
A1: rng R c= HFuncs X and
A2: for f, g being homogeneous Function st f in rng R & g in rng R holds
arity f = arity g ; :: 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 ) ) ) )
assume A3: ( f in rng R & g in rng R ) ; :: thesis: ( ( 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 ) ) )
then reconsider f' = f, g' = g as Element of HFuncs X by A1;
A4: arity f' = arity g' by A2, A3;

hereby :: thesis: ( 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 ) )

assume f is empty ; :: thesis: ( g is empty or dom g = {{} } )
then dom g' c= 0 -tuples_on X by A4, Th21, Th23;
then dom g' c= {(<*> X)} by FINSEQ_2:112;
then ( dom g = {} or dom g = {{} } ) by ZFMISC_1:39;
hence ( g is empty or dom g = {{} } ) ; :: thesis: verum

end;

assume ( not f is empty & not g is empty ) ; :: thesis: 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 )
then reconsider f' = f' as non empty Element of HFuncs X ;
take n = arity f'; :: thesis: ex X being non empty set st
( dom f c= n -tuples_on X & dom g c= n -tuples_on X )
take X ; :: thesis: ( dom f c= n -tuples_on X & dom g c= n -tuples_on X )
thus ( dom f c= n -tuples_on X & dom g c= n -tuples_on X ) by A4, Th23; :: thesis: verum