hereby :: thesis:

given f being homogeneous Function such that A1: f in rng F ; :: thesis:
take i = arity f; :: thesis:
let g be homogeneous Function; :: thesis:
assume A2: g in rng F ; :: thesis:

per cases ;

suppose A3: f is empty ; :: thesis:

thus i = arity g :: thesis:

proof

per cases by A1, A2, A3, Def3;

suppose g is empty ; :: thesis:

hence i = arity g by A3; :: thesis:

end;

suppose dom g = {{}} ; :: thesis:

hence i = arity g by A3, Th17, Th18; :: thesis:

end;

end;

end;

end;

suppose A4: g is empty ; :: thesis:

thus i = arity g :: thesis:

proof

per cases by A1, A2, A4, Def3;

suppose f is empty ; :: thesis:

hence i = arity g by A4; :: thesis:

end;

suppose dom f = {{}} ; :: thesis:

hence i = arity g by A4, Th17, Th18; :: thesis:

end;

end;

end;

end;

suppose A5: ( not f is empty & not g is empty ) ; :: thesis:

set a = the Element of dom f;
dom f <> {} by A5;
then A6: the Element of dom f in dom f ;
consider n being Element of NAT , X being non empty set such that
A7: dom f c= n -tuples_on X and
A8: dom g c= n -tuples_on X by A1, A2, A5, Def3;
reconsider a = the Element of dom f as Element of n -tuples_on X by A7, A6;
A9: arity f = len a by A5, MARGREL1:def 25
.= n by CARD_1:def 7 ;
set a = the Element of dom g;
dom g <> {} by A5;
then the Element of dom g in dom g ;
then reconsider a = the Element of dom g as Element of n -tuples_on X by A8;
arity g = len a by A5, MARGREL1:def 25;
hence i = arity g by A9, CARD_1:def 7; :: thesis:

end;

end;

end;

thus ( ( for f being homogeneous Function holds not f in rng F ) implies ex b₁ being Element of NAT st b₁ = 0 ) ; :: thesis: