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 X = S by PARTFUN1:def 2;
A3: dom Y = S by PARTFUN1:def 2;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Union (coprod X) or x in Union (coprod Y) )
assume A4: x in Union (coprod X) ; :: thesis: x in Union (coprod Y)
then A5: x `2 in dom X by CARD_3:22;
A6: x `1 in X . (x `2) by A4, CARD_3:22;
A7: x = [(x `1),(x `2)] by A4, CARD_3:22;
X . (x `2) c= Y . (x `2) by A1, A2, A5, PBOOLE:def 2;
hence x in Union (coprod Y) by A2, A3, A5, A6, A7, CARD_3:22; :: thesis: verum