for n being Nat holds
( F₁(n) in F₂() iff n < card F₂() )

A1: for x being set st x in F₂() holds
ex n being Nat st x = F₁(n) and
A2: for i, j being Nat st i < j & F₁(j) in F₂() holds
F₁(i) in F₂() and
A3: for i, j being Nat st F₁(i) = F₁(j) holds
i = j