let X be set ; :: thesis: for f, g being FinSequence st f ^ g is X -valued holds
( f is X -valued & g is X -valued )
let f, g be FinSequence; :: thesis: ( f ^ g is X -valued implies ( f is X -valued & g is X -valued ) )
set h = f ^ g;
assume f ^ g is X -valued ; :: thesis: ( f is X -valued & g is X -valued )
then A1: rng (f ^ g) c= X by RELAT_1:def 19;
( rng f c= rng (f ^ g) & rng g c= rng (f ^ g) ) by FINSEQ_1:29, FINSEQ_1:30;
then ( rng f c= X & rng g c= X ) by A1;
hence ( f is X -valued & g is X -valued ) by RELAT_1:def 19; :: thesis: verum