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