scheme :: BIRKHOFF:sch 11
FreeInModIsInVar{ F₁() -> non empty non void ManySortedSign , F₂() -> strict non-empty MSAlgebra over F₁(), F₃() -> ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of F₂(), P₁[ set ], P₂[ set ] } :

P₁[F₂()]

provided

A1: for A being non-empty MSAlgebra over F₁() holds
( P₂[A] iff for s being SortSymbol of F₁()
for e being Element of (Equations F₁()) . s st ( for B being non-empty MSAlgebra over F₁() st P₁[B] holds
B |= e ) holds
A |= e ) and
A2: for C being non-empty MSAlgebra over F₁()
for G being ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of C st P₂[C] holds
ex H being ManySortedFunction of F₂(),C st
( H is_homomorphism F₂(),C & H ** F₃() = G & ( for K being ManySortedFunction of F₂(),C st K is_homomorphism F₂(),C & K ** F₃() = G holds
H = K ) ) and
A3: P₂[F₂()] and
A4: for A, B being non-empty MSAlgebra over F₁() st A,B are_isomorphic & P₁[A] holds
P₁[B] and
A5: for A being non-empty MSAlgebra over F₁()
for B being strict non-empty MSSubAlgebra of A st P₁[A] holds
P₁[B] and
A6: 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]