let J be non empty non void Signature; for X being V3() ManySortedSet of the carrier of J
for Q being SubstMSAlgebra over J,X st X is ManySortedSubset of the Sorts of Q holds
for a being SortSymbol of J st the Sorts of Q . a <> {} holds
for A being Element of Q,a
for x, y being Element of Union X
for t being Element of Union the Sorts of Q st y = t holds
for j being SortSymbol of J st x in X . j & y in X . j holds
A / (x,y) = A / (x,t)
let X be V3() ManySortedSet of the carrier of J; for Q being SubstMSAlgebra over J,X st X is ManySortedSubset of the Sorts of Q holds
for a being SortSymbol of J st the Sorts of Q . a <> {} holds
for A being Element of Q,a
for x, y being Element of Union X
for t being Element of Union the Sorts of Q st y = t holds
for j being SortSymbol of J st x in X . j & y in X . j holds
A / (x,y) = A / (x,t)
let Q be SubstMSAlgebra over J,X; ( X is ManySortedSubset of the Sorts of Q implies for a being SortSymbol of J st the Sorts of Q . a <> {} holds
for A being Element of Q,a
for x, y being Element of Union X
for t being Element of Union the Sorts of Q st y = t holds
for j being SortSymbol of J st x in X . j & y in X . j holds
A / (x,y) = A / (x,t) )
assume A1:
X is ManySortedSubset of the Sorts of Q
; for a being SortSymbol of J st the Sorts of Q . a <> {} holds
for A being Element of Q,a
for x, y being Element of Union X
for t being Element of Union the Sorts of Q st y = t holds
for j being SortSymbol of J st x in X . j & y in X . j holds
A / (x,y) = A / (x,t)
let a be SortSymbol of J; ( the Sorts of Q . a <> {} implies for A being Element of Q,a
for x, y being Element of Union X
for t being Element of Union the Sorts of Q st y = t holds
for j being SortSymbol of J st x in X . j & y in X . j holds
A / (x,y) = A / (x,t) )
assume A2:
the Sorts of Q . a <> {}
; for A being Element of Q,a
for x, y being Element of Union X
for t being Element of Union the Sorts of Q st y = t holds
for j being SortSymbol of J st x in X . j & y in X . j holds
A / (x,y) = A / (x,t)
let A be Element of Q,a; for x, y being Element of Union X
for t being Element of Union the Sorts of Q st y = t holds
for j being SortSymbol of J st x in X . j & y in X . j holds
A / (x,y) = A / (x,t)
let x, y be Element of Union X; for t being Element of Union the Sorts of Q st y = t holds
for j being SortSymbol of J st x in X . j & y in X . j holds
A / (x,y) = A / (x,t)
let t be Element of Union the Sorts of Q; ( y = t implies for j being SortSymbol of J st x in X . j & y in X . j holds
A / (x,y) = A / (x,t) )
assume A3:
y = t
; for j being SortSymbol of J st x in X . j & y in X . j holds
A / (x,y) = A / (x,t)
let j be SortSymbol of J; ( x in X . j & y in X . j implies A / (x,y) = A / (x,t) )
assume A4:
x in X . j
; ( not y in X . j or A / (x,y) = A / (x,t) )
assume A5:
y in X . j
; A / (x,y) = A / (x,t)
A6:
X . j is Subset of ( the Sorts of Q . j)
by A1, Th13;
thus A / (x,y) =
the subst-op of Q . [A,[x,y]]
by A1, A2, A4, A5, Def12
.=
A / (x,t)
by A6, A5, A3, A4, A2, Def13
; verum