let J be non empty non void Signature; :: thesis: for X being empty-yielding 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 empty-yielding 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 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 ; :: thesis: verum