scheme :: FUNCT_7:sch 7
Unionx{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃() -> Element of F₁(), F₄() -> F₁() -valued Function, F₅() -> object , F₆( object ) -> object } :

{ F₆(i) where i is Element of F₁() : i in rng F₄() } = { F₆(j) where j is Element of F₁() : j in rng (F₄() +* (F₅(),F₂())) }

provided

A1: F₆(F₃()) = F₆(F₂()) and
A2: F₃() = F₄() . F₅()