let J be non empty non void Signature; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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 <> {} ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( x in X . j & y in X . j implies A / (x,y) = A / (x,t) )
assume A4: x in X . j ; :: thesis: ( not y in X . j or A / (x,y) = A / (x,t) )
assume A5: y in X . j ; :: thesis: A / (x,y) = A / (x,t)
A6: X . j is Subset of ( the Sorts of Q . j) by ;
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 ; :: thesis: verum