A1: dom (s1 + s2) = (dom s1) /\ (dom s2) by VALUED_1:def 1
.= NAT /\ (dom s2) by FUNCT_2:def 1
.= NAT /\ NAT by FUNCT_2:def 1 ;

now :: thesis: for x being object st x in NAT holds
(s1 + s2) . x in X

let x be object ; :: thesis: ( x in NAT implies (s1 + s2) . x in X )
assume A2: x in NAT ; :: thesis: (s1 + s2) . x in X
A3: ( s1 . x in X & s2 . x in X ) by A2, FUNCT_2:5;
(s1 + s2) . x = (s1 . x) + (s2 . x) by A1, A2, VALUED_1:def 1;
hence (s1 + s2) . x in X by A3, MEMBERED:def 25; :: thesis: verum

end;

hence s1 + s2 is sequence of X by A1, FUNCT_2:3; :: thesis: verum