let S be set ; :: thesis: 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; :: thesis: ( X c= Y implies Union (coprod X) c= Union (coprod Y) )
assume A1: X c= Y ; :: thesis: Union (coprod X) c= Union (coprod Y)
A2: dom Y = S by PARTFUN1:def 2;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Union (coprod X) or x in Union (coprod Y) )
assume A3: x in Union (coprod X) ; :: thesis: 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; :: thesis: verum