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 that
A3: f in rng R and
A4: 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 ) ) )
reconsider f' = f, g' = g as Element of HFuncs X by A1, A3, A4;
A5: arity f' = arity g' by A2, A3, A4;

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 A5, Th21, Th23;
then dom g' c= {(<*> X)} by FINSEQ_2:112;
hence ( g is empty or dom g = {{} } ) by ZFMISC_1:39; :: thesis: verum

end;

assume that
A6: not f is empty and
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 )
reconsider f' = f' as non empty Element of HFuncs X by A6;
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 A5, Th23; :: thesis: verum