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