let D, D9, E be non empty set ; :: thesis: for r being FinSequence
for F being Function of [:D,D9:],E
for p being FinSequence of D
for q being FinSequence of D9 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,D9:],E
for p being FinSequence of D
for q being FinSequence of D9 st len p = len q & r = F .: (p,q) holds
( len r = len p & len r = len q )
let F be Function of [:D,D9:],E; :: thesis: for p being FinSequence of D
for q being FinSequence of D9 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 D9 st len p = len q & r = F .: (p,q) holds
( len r = len p & len r = len q )
let q be FinSequence of D9; :: 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