let X be non empty set ; 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; ( 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
; R is with_the_same_arity
let f, g be Function; COMPUT_1:def 3 ( 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
; ( ( 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 f9 = f, g9 = g as Element of HFuncs X by A1, A3, A4;
A5:
arity f9 = arity g9
by A2, A3, A4;
assume that
A6:
not f is empty
and
not g is empty
; 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 f9 = f9 as non empty Element of HFuncs X by A6;
take
arity f9
; ex X being non empty set st
( dom f c= (arity f9) -tuples_on X & dom g c= (arity f9) -tuples_on X )
take
X
; ( dom f c= (arity f9) -tuples_on X & dom g c= (arity f9) -tuples_on X )
thus
( dom f c= (arity f9) -tuples_on X & dom g c= (arity f9) -tuples_on X )
by A5, Th19; verum