let X, Y be natural-membered finite 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 Th31;
then (Sgm0 Y) . 0 = (Sgm0 (X \/ Y)) . (0 + (len (Sgm0 X))) by A2, Th42;
hence (Sgm0 Y) . 0 = (Sgm0 (X \/ Y)) . (len (Sgm0 X)) ; :: thesis: verum