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

given f being homogeneous Function such that A1: f in rng F ; :: thesis: ex i being Element of omega st
for g being homogeneous Function st g in rng F holds
b₃ = arity b₄
take i = arity f; :: thesis: for g being homogeneous Function st g in rng F holds
b₂ = arity b₃
let g be homogeneous Function; :: thesis: ( g in rng F implies b₁ = arity b₂ )
assume A2: g in rng F ; :: thesis: b₁ = arity b₂

per cases ( f is empty or g is empty or ( not f is empty & not g is empty ) ) ;

suppose A3: f is empty ; :: thesis: b₁ = arity b₂

thus i = arity g :: thesis: verum

proof

per cases ( g is empty or dom g = {{}} ) by A1, A2, A3, Def3;

suppose g is empty ; :: thesis: i = arity g

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

end;

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

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

end;

end;

end;

end;

suppose A4: g is empty ; :: thesis: b₁ = arity b₂

thus i = arity g :: thesis: verum

proof

per cases ( f is empty or dom f = {{}} ) by A1, A2, A4, Def3;

suppose f is empty ; :: thesis: i = arity g

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

end;

suppose dom f = {{}} ; :: thesis: i = arity g

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

end;

end;

end;

end;

suppose A5: ( not f is empty & not g is empty ) ; :: thesis: b₁ = arity b₂

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: verum

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: verum