scheme :: BIRKHOFF:sch 2
ExFreeAlg2{ F₁() -> non empty non void ManySortedSign , F₂() -> non-empty ManySortedSet of the carrier of F₁(), P₁[ set ] } :

ex A being strict non-empty MSAlgebra over F₁() ex F being ManySortedFunction of F₂(), the Sorts of A st
( P₁[A] & ( for B being non-empty MSAlgebra over F₁()
for G being ManySortedFunction of F₂(), the Sorts of B st P₁[B] holds
ex H being ManySortedFunction of A,B st
( H is_homomorphism A,B & H ** F = G & ( for K being ManySortedFunction of A,B st K is_homomorphism A,B & K ** F = G holds
H = K ) ) ) )

provided

A1: for A, B being non-empty MSAlgebra over F₁() st A,B are_isomorphic & P₁[A] holds
P₁[B] and
A2: for A being non-empty MSAlgebra over F₁()
for B being strict non-empty MSSubAlgebra of A st P₁[A] holds
P₁[B] and
A3: for I being set
for F being MSAlgebra-Family of I,F₁() st ( for i being set st i in I holds
ex A being MSAlgebra over F₁() st
( A = F . i & P₁[A] ) ) holds
P₁[ product F]