let X, Y be finite natural-membered set ; :: thesis: rng ((Sgm0 X) ^ (Sgm0 Y)) = rng (Sgm0 (X \/ Y))
thus rng ((Sgm0 X) ^ (Sgm0 Y)) = (rng (Sgm0 X)) \/ (rng (Sgm0 Y)) by AFINSQ_1:26
.= X \/ (rng (Sgm0 Y)) by AFINSQ_2:def 4
.= X \/ Y by AFINSQ_2:def 4
.= rng (Sgm0 (X \/ Y)) by AFINSQ_2:def 4 ; :: thesis: verum