let D, D', E be non empty set ; :: thesis: for r being FinSequence
for F being Function of [:D,D':],E
for p being FinSequence of D
for q being FinSequence of D' st len p = len q & r = F .: p,q holds
( len r = len p & len r = len q )
let r be FinSequence; :: thesis: for F being Function of [:D,D':],E
for p being FinSequence of D
for q being FinSequence of D' st len p = len q & r = F .: p,q holds
( len r = len p & len r = len q )
let F be Function of [:D,D':],E; :: thesis: for p being FinSequence of D
for q being FinSequence of D' st len p = len q & r = F .: p,q holds
( len r = len p & len r = len q )
let p be FinSequence of D; :: thesis: for q being FinSequence of D' st len p = len q & r = F .: p,q holds
( len r = len p & len r = len q )
let q be FinSequence of D'; :: thesis: ( len p = len q & r = F .: p,q implies ( len r = len p & len r = len q ) )
assume that
A1: len p = len q and
A2: r = F .: p,q ; :: thesis: ( len r = len p & len r = len q )
len r = min (len p),(len q) by A2, Th85;
hence ( len r = len p & len r = len q ) by A1; :: thesis: verum