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