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 RELAT_1:def 19;
then A1: (rng p) \/ (rng q) c= D by Th24;
rng p c= (rng p) \/ (rng q) by XBOOLE_1:7;
then rng p c= D by A1;
hence p is XFinSequence of D by RELAT_1:def 19; :: thesis: q is XFinSequence of D
rng q c= (rng p) \/ (rng q) by XBOOLE_1:7;
then rng q c= D by A1;
hence q is XFinSequence of D by RELAT_1:def 19; :: thesis: verum