let p, q be FinSequence; :: thesis: for D being set st p ^ q is FinSequence of D holds
( p is FinSequence of D & q is FinSequence of D )
let D be set ; :: thesis: ( p ^ q is FinSequence of D implies ( p is FinSequence of D & q is FinSequence of D ) )
assume p ^ q is FinSequence of D ; :: thesis: ( p is FinSequence of D & q is FinSequence of D )
then rng (p ^ q) c= D by Def4;
then A1: (rng p) \/ (rng q) c= D by Th44;
rng p c= (rng p) \/ (rng q) by XBOOLE_1:7;
then rng p c= D by A1, XBOOLE_1:1;
hence p is FinSequence of D by Def4; :: thesis: q is FinSequence 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 FinSequence of D by Def4; :: thesis: verum