let A, B be set ; :: thesis: for F being ManySortedSet of [:B,A:]
for C being Subset of A
for D being Subset of B
for x, y being set st x in C & y in D holds
F . y,x = (F | [:D,C:]) . y,x
let F be ManySortedSet of [:B,A:]; :: thesis: for C being Subset of A
for D being Subset of B
for x, y being set st x in C & y in D holds
F . y,x = (F | [:D,C:]) . y,x
let C be Subset of A; :: thesis: for D being Subset of B
for x, y being set st x in C & y in D holds
F . y,x = (F | [:D,C:]) . y,x
let D be Subset of B; :: thesis: for x, y being set st x in C & y in D holds
F . y,x = (F | [:D,C:]) . y,x
let x, y be set ; :: thesis: ( x in C & y in D implies F . y,x = (F | [:D,C:]) . y,x )
assume ( x in C & y in D ) ; :: thesis: F . y,x = (F | [:D,C:]) . y,x
then [y,x] in [:D,C:] by ZFMISC_1:106;
hence F . y,x = (F | [:D,C:]) . y,x by FUNCT_1:72; :: thesis: verum