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:87;
hence F . (y,x) = (F | [:D,C:]) . (y,x) by FUNCT_1:49; :: thesis: verum