F₄() .:.: F₂() is V2() GeneratorSet of F₃()

A1: for C being non-empty MSAlgebra over F₁()
for G being ManySortedFunction of F₂(), 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
A2: P₁[F₃()] and
A3: for A being non-empty MSAlgebra over F₁()
for B being strict non-empty MSSubAlgebra of A st P₁[A] holds
P₁[B]