let i be natural Number ; for p, q being FinSequence
for F being Function st [:(rng p),(rng q):] c= dom F & i = min ((len p),(len q)) holds
dom (F .: (p,q)) = Seg i
let p, q be FinSequence; for F being Function st [:(rng p),(rng q):] c= dom F & i = min ((len p),(len q)) holds
dom (F .: (p,q)) = Seg i
let F be Function; ( [:(rng p),(rng q):] c= dom F & i = min ((len p),(len q)) implies dom (F .: (p,q)) = Seg i )
assume that
A1:
[:(rng p),(rng q):] c= dom F
and
A2:
i = min ((len p),(len q))
; dom (F .: (p,q)) = Seg i
A3:
( rng <:p,q:> c= [:(rng p),(rng q):] & dom <:p,q:> = (dom p) /\ (dom q) )
by FUNCT_3:51, FUNCT_3:def 7;
( dom p = Seg (len p) & dom q = Seg (len q) )
by FINSEQ_1:def 3;
then
(dom p) /\ (dom q) = Seg i
by A2, Th1;
hence
dom (F .: (p,q)) = Seg i
by A1, A3, RELAT_1:27, XBOOLE_1:1; verum