let X, Y be finite natural-membered set ; :: thesis: ( Y <> {} & X <N< Y implies (Sgm0 Y) . 0 = (Sgm0 (X \/ Y)) . (len (Sgm0 X)) )
assume that
A1: Y <> {} and
A2: X <N< Y ; :: thesis: (Sgm0 Y) . 0 = (Sgm0 (X \/ Y)) . (len (Sgm0 X))
card Y <> 0 by A1;
then 0 < len (Sgm0 Y) by Th20;
then (Sgm0 Y) . 0 = (Sgm0 (X \/ Y)) . (0 + (len (Sgm0 X))) by A2, Th31;
hence (Sgm0 Y) . 0 = (Sgm0 (X \/ Y)) . (len (Sgm0 X)) ; :: thesis: verum