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 ;

.= 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

hence
s1 + s2 is sequence of X
by A1, FUNCT_2:3; :: thesis: verum(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;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