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 NAT 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, Def6;

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, Th21, Th22; :: 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, Def6;

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, Th21, Th22; :: thesis: verum

end;

end;

end;

end;

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

then consider n being Element of NAT , X being non empty set such that
A6: ( dom f c= n -tuples_on X & dom g c= n -tuples_on X ) by A1, A2, Def6;
consider a being Element of dom f;
A7: dom f <> {} by A5;
then a in dom f ;
then reconsider a = a as Element of n -tuples_on X by A6;
A8: arity f = len a by A7, UNIALG_1:def 10
.= n by FINSEQ_1:def 18 ;
consider a being Element of dom g;
A9: dom g <> {} by A5;
then a in dom g ;
then reconsider a = a as Element of n -tuples_on X by A6;
arity g = len a by A9, UNIALG_1:def 10;
hence i = arity g by A8, FINSEQ_1:def 18; :: 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