assume 0 in rng (s1 ^ s2) ; :: according to ORDINAL1:def 15 :: thesis: contradiction
then 0 in (rng s1) \/ (rng s2) by ORDINAL4:2;
then ( 0 in rng s1 or 0 in rng s2 ) by XBOOLE_0:def 3;
hence contradiction ; :: thesis: verum