let i be natural Number ; :: thesis: 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; :: thesis: 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; :: thesis: ( [:(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)) ; :: thesis: 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; :: thesis: verum