scheme :: BIRKHOFF:sch 10
FreeInModIsInVar1{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra over F1(), P1[ set ], P2[ set ] } :
P2[F2()]
provided
A1: for A being non-empty MSAlgebra over F1() holds
( P2[A] iff for s being SortSymbol of F1()
for e being Element of (Equations F1()) . s st ( for B being non-empty MSAlgebra over F1() st P1[B] holds
B |= e ) holds
A |= e ) and
A2: P1[F2()]