let S be set ; for X, Y being ManySortedSet of S st X c= Y holds
Union (coprod X) c= Union (coprod Y)
let X, Y be ManySortedSet of S; ( X c= Y implies Union (coprod X) c= Union (coprod Y) )
assume A1:
X c= Y
; Union (coprod X) c= Union (coprod Y)
A2:
dom Y = S
by PARTFUN1:def 2;
let x be object ; TARSKI:def 3 ( not x in Union (coprod X) or x in Union (coprod Y) )
assume A3:
x in Union (coprod X)
; x in Union (coprod Y)
then A4:
x `2 in dom X
by CARD_3:22;
A5:
x `1 in X . (x `2)
by A3, CARD_3:22;
A6:
x = [(x `1),(x `2)]
by A3, CARD_3:22;
X . (x `2) c= Y . (x `2)
by A1, A4;
hence
x in Union (coprod Y)
by A2, A4, A5, A6, CARD_3:22; verum