let X, Y be finite natural-membered set ; :: thesis: ( X misses Y implies dom ((Sgm0 X) ^ (Sgm0 Y)) = dom (Sgm0 (X \/ Y)) )

assume A1: X misses Y ; :: thesis: dom ((Sgm0 X) ^ (Sgm0 Y)) = dom (Sgm0 (X \/ Y))

thus dom ((Sgm0 X) ^ (Sgm0 Y)) = (len (Sgm0 X)) + (len (Sgm0 Y)) by AFINSQ_1:def 3

.= (card X) + (len (Sgm0 Y)) by AFINSQ_2:20

.= (card X) + (card Y) by AFINSQ_2:20

.= card (X \/ Y) by A1, CARD_2:40

.= len (Sgm0 (X \/ Y)) by AFINSQ_2:20

.= dom (Sgm0 (X \/ Y)) ; :: thesis: verum

assume A1: X misses Y ; :: thesis: dom ((Sgm0 X) ^ (Sgm0 Y)) = dom (Sgm0 (X \/ Y))

thus dom ((Sgm0 X) ^ (Sgm0 Y)) = (len (Sgm0 X)) + (len (Sgm0 Y)) by AFINSQ_1:def 3

.= (card X) + (len (Sgm0 Y)) by AFINSQ_2:20

.= (card X) + (card Y) by AFINSQ_2:20

.= card (X \/ Y) by A1, CARD_2:40

.= len (Sgm0 (X \/ Y)) by AFINSQ_2:20

.= dom (Sgm0 (X \/ Y)) ; :: thesis: verum