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

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