let p, q be FinSequence; :: thesis: for F being Function st [:(rng p),(rng q):] c= dom F holds
F .: p,q is FinSequence
let F be Function; :: thesis: ( [:(rng p),(rng q):] c= dom F implies F .: p,q is FinSequence )
reconsider k = min (len p),(len q) as Element of NAT by XXREAL_0:15;
assume [:(rng p),(rng q):] c= dom F ; :: thesis: F .: p,q is FinSequence
then dom (F .: p,q) = Seg k by Lm3;
hence F .: p,q is FinSequence by FINSEQ_1:def 2; :: thesis: verum