for s being SortSymbol of F₁()
for e being Element of (Equations F₁()) . s st ( for B being non-empty MSAlgebra of F₁() st P₁[B] holds
B |= e ) holds
F₂() |= e by A2;
hence P₂[F₂()] by A1; :: thesis: verum