let f, g be non empty Element of HFuncs NAT; :: thesis: for F being with_the_same_arity FinSequence of HFuncs NAT st g = f * <:F:> holds
arity g = arity F
let F be with_the_same_arity FinSequence of HFuncs NAT; :: thesis: ( g = f * <:F:> implies arity g = arity F )
assume g = f * <:F:> ; :: thesis: arity g = arity F
then A1: dom g c= (arity F) -tuples_on NAT by Th41;
consider x being object such that
A2: x in dom g by XBOOLE_0:def 1;
reconsider x = x as Element of (arity F) -tuples_on NAT by A1, A2;
len x = arity F by CARD_1:def 7;
hence arity g = arity F by A2, MARGREL1:def 25; :: thesis: verum