let I be set ; :: thesis: for X, Y being ManySortedSet of I
for i being set st i in I holds
(X \+\ Y) . i = (X . i) \+\ (Y . i)
let X, Y be ManySortedSet of I; :: thesis: for i being set st i in I holds
(X \+\ Y) . i = (X . i) \+\ (Y . i)
let i be set ; :: thesis: ( i in I implies (X \+\ Y) . i = (X . i) \+\ (Y . i) )
assume A1: i in I ; :: thesis: (X \+\ Y) . i = (X . i) \+\ (Y . i)
thus (X \+\ Y) . i = ((X \ Y) . i) \/ ((Y \ X) . i) by A1, Def7
.= ((X . i) \ (Y . i)) \/ ((Y \ X) . i) by A1, Def9
.= (X . i) \+\ (Y . i) by A1, Def9 ; :: thesis: verum