scheme :: MSAFREE1:sch 2
FreeSortUniq{ F₁() -> non empty non void ManySortedSign , F₂() -> non-empty ManySortedSet of the carrier of F₁(), F₃() -> non-empty ManySortedSet of the carrier of F₁(), F₄( set ) -> Element of Union F₃(), F₅( object , object , object ) -> Element of Union F₃(), F₆() -> ManySortedFunction of FreeSort F₂(),F₃(), F₇() -> ManySortedFunction of FreeSort F₂(),F₃() } :

F₆() = F₇()

provided

A1: for o being OperSymbol of F₁()
for ts being Element of Args (o,(FreeMSA F₂()))
for x being Element of (Union F₃()) * st x = (Flatten F₆()) * ts holds
(F₆() . (the_result_sort_of o)) . ((Den (o,(FreeMSA F₂()))) . ts) = F₅(o,ts,x) and
A2: for s being SortSymbol of F₁()
for y being set st y in FreeGen (s,F₂()) holds
(F₆() . s) . y = F₄(y) and
A3: for o being OperSymbol of F₁()
for ts being Element of Args (o,(FreeMSA F₂()))
for x being Element of (Union F₃()) * st x = (Flatten F₇()) * ts holds
(F₇() . (the_result_sort_of o)) . ((Den (o,(FreeMSA F₂()))) . ts) = F₅(o,ts,x) and
A4: for s being SortSymbol of F₁()
for y being set st y in FreeGen (s,F₂()) holds
(F₇() . s) . y = F₄(y)