scheme :: MSAFREE1:sch 3
ExtFreeGen{ F₁() -> non empty non void ManySortedSign , F₂() -> V2() ManySortedSet of the carrier of F₁(), F₃() -> non-empty MSAlgebra over F₁(), P₁[ object , object , object ], F₄() -> ManySortedFunction of (FreeMSA F₂()),F₃(), F₅() -> ManySortedFunction of (FreeMSA F₂()),F₃() } :

F₄() = F₅()

provided

A1: F₄() is_homomorphism FreeMSA F₂(),F₃() and
A2: for s being SortSymbol of F₁()
for x, y being set st y in FreeGen (s,F₂()) holds
( (F₄() . s) . y = x iff P₁[s,x,y] ) and
A3: F₅() is_homomorphism FreeMSA F₂(),F₃() and
A4: for s being SortSymbol of F₁()
for x, y being set st y in FreeGen (s,F₂()) holds
( (F₅() . s) . y = x iff P₁[s,x,y] )