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 A1: g = f * <:F:> ; :: thesis: arity g = arity F
A2: dom g c= (arity F) -tuples_on NAT by A1, Th46;
consider x being set such that
A3: x in dom g by XBOOLE_0:def 1;
reconsider x = x as Element of (arity F) -tuples_on NAT by A2, A3;
len x = arity F by FINSEQ_2:109;
hence arity g = arity F by A3, UNIALG_1:def 10; :: thesis: verum