let p, q be XFinSequence; :: thesis: for D being set st p ^ q is XFinSequence of D holds
( p is XFinSequence of D & q is XFinSequence of D )
let D be set ; :: thesis: ( p ^ q is XFinSequence of D implies ( p is XFinSequence of D & q is XFinSequence of D ) )
assume p ^ q is XFinSequence of D ; :: thesis: ( p is XFinSequence of D & q is XFinSequence of D )
then rng (p ^ q) c= D by ORDINAL1:def 8;
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 D by ORDINAL1:def 8; :: thesis: q is XFinSequence of D
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 D by ORDINAL1:def 8; :: thesis: verum