ex F being XFinSequence of NAT st
( dom F = card F₂() & card { g where g is Function of F₁(),F₂() : P₁[g] } = Sum F & ( for i being Nat st i in dom F holds
F . i = card { g where g is Function of F₁(),F₂() : ( P₁[g] & g . F₃() = F₄() . i ) } ) )

A1: ( F₄() is onto & F₄() is one-to-one ) and
A2: not F₂() is empty and
A3: F₃() in F₁()