let I be set ; :: thesis: for p, q being FinSequence st p ^ q is I -valued holds
( p is I -valued & q is I -valued )
let p, q be FinSequence; :: thesis: ( p ^ q is I -valued implies ( p is I -valued & q is I -valued ) )
assume Z1: rng (p ^ q) c= I ; :: according to RELAT_1:def 19 :: thesis: ( p is I -valued & q is I -valued )
A1: rng (p ^ q) = (rng p) \/ (rng q) by FINSEQ_1:31;
rng p c= (rng p) \/ (rng q) by XBOOLE_1:7;
hence rng p c= I by Z1, A1, XBOOLE_1:1; :: according to RELAT_1:def 19 :: thesis: q is I -valued
rng q c= (rng p) \/ (rng q) by XBOOLE_1:7;
hence rng q c= I by Z1, A1, XBOOLE_1:1; :: according to RELAT_1:def 19 :: thesis: verum