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