theorem
for
n being non
empty Nat for
J being non
empty non
void Signature for
T being
non-empty MSAlgebra over
J for
X being
empty-yielding GeneratorSet of
T for
S1 being non
empty non
void b2 -extension b1 PC-correct QC-correct QCLangSignature over
Union X for
x0 being
Element of
Union (X extended_by ({}, the carrier of S1)) for
L being
non-empty Language of
X extended_by (
{}, the
carrier of
S1),
S1 for
G1 being
QC-theory_with_equality of
L for
s,
s1 being
SortSymbol of
S1 for
t being
Element of
L,
s for
t1,
t2 being
Element of
L,
s1 st
L is
subst-eq-correct &
x0 in X . s &
t1 '=' (
t2,
L)
in G1 holds
(t1 / (x0,t)) '=' (
(t2 / (x0,t)),
L)
in G1