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 3 :: 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 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 ; :: 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 f9 = f9 as non empty Element of HFuncs X by A6;
take arity f9 ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: verum