let p, q, r be FinSequence; 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; ( [:(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
; ( 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; verum