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