let p, q be XFinSequence; :: thesis: for D being set st p ^ q is XFinSequence of holds
( p is XFinSequence of & q is XFinSequence of )
let D be set ; :: thesis: ( p ^ q is XFinSequence of implies ( p is XFinSequence of & q is XFinSequence of ) )
assume p ^ q is XFinSequence of ; :: thesis: ( p is XFinSequence of & q is XFinSequence of )
then rng (p ^ q) c= D by RELAT_1:def 19;
then A1: (rng p) \/ (rng q) c= D by Th29;
rng p c= (rng p) \/ (rng q) by XBOOLE_1:7;
then rng p c= D by A1, XBOOLE_1:1;
hence p is XFinSequence of by RELAT_1:def 19; :: thesis: q is XFinSequence of
rng q c= (rng p) \/ (rng q) by XBOOLE_1:7;
then rng q c= D by A1, XBOOLE_1:1;
hence q is XFinSequence of by RELAT_1:def 19; :: thesis: verum