let i be Nat; :: 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:71, FUNCT_3:def 8;
A4: F .: p,q = F * <:p,q:> by FUNCOP_1:def 3;
( dom p = Seg (len p) & dom q = Seg (len q) ) by FINSEQ_1:def 3;
then (dom p) /\ (dom q) = Seg i by A2, Th2;
hence dom (F .: p,q) = Seg i by A1, A3, A4, RELAT_1:46, XBOOLE_1:1; :: thesis: verum