let P1, P2 be Subset of (TOP-REAL 2); :: thesis: ( ( for i1, j1, i2, j2 being Nat st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & P1 = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & P1 = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & P1 = cell ((GoB f),i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & P1 = cell ((GoB f),(i1 -' 1),j2) ) ) & ( for i1, j1, i2, j2 being Nat st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & P2 = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & P2 = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & P2 = cell ((GoB f),i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & P2 = cell ((GoB f),(i1 -' 1),j2) ) ) implies P1 = P2 )
assume that
A39: for i1, j1, i2, j2 being Nat st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & P1 = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & P1 = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & P1 = cell ((GoB f),i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & P1 = cell ((GoB f),(i1 -' 1),j2) ) and
A40: for i1, j1, i2, j2 being Nat st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * (i1,j1) & f /. (k + 1) = (GoB f) * (i2,j2) & not ( i1 = i2 & j1 + 1 = j2 & P2 = cell ((GoB f),i1,j1) ) & not ( i1 + 1 = i2 & j1 = j2 & P2 = cell ((GoB f),i1,(j1 -' 1)) ) & not ( i1 = i2 + 1 & j1 = j2 & P2 = cell ((GoB f),i2,j2) ) holds
( i1 = i2 & j1 = j2 + 1 & P2 = cell ((GoB f),(i1 -' 1),j2) ) ; :: thesis: P1 = P2

per cases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A10;

suppose ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis: P1 = P2

then A41: j1 < j2 by XREAL_1:29;
A42: j2 <= j2 + 1 by NAT_1:11;
hence P1 = cell ((GoB f),i1,j1) by A4, A5, A7, A8, A39, A41
.= P2 by A4, A5, A7, A8, A40, A41, A42 ;
:: thesis: verum

end;

suppose ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis: P1 = P2

then A43: i1 < i2 by XREAL_1:29;
A44: i2 <= i2 + 1 by NAT_1:11;
hence P1 = cell ((GoB f),i1,(j1 -' 1)) by A4, A5, A7, A8, A39, A43
.= P2 by A4, A5, A7, A8, A40, A43, A44 ;
:: thesis: verum

end;

suppose ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis: P1 = P2

then A45: i2 < i1 by XREAL_1:29;
A46: i1 <= i1 + 1 by NAT_1:11;
hence P1 = cell ((GoB f),i2,j2) by A4, A5, A7, A8, A39, A45
.= P2 by A4, A5, A7, A8, A40, A45, A46 ;
:: thesis: verum

end;

suppose ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis: P1 = P2

then A47: j2 < j1 by XREAL_1:29;
A48: j1 <= j1 + 1 by NAT_1:11;
hence P1 = cell ((GoB f),(i1 -' 1),j2) by A4, A5, A7, A8, A39, A47
.= P2 by A4, A5, A7, A8, A40, A47, A48 ;
:: thesis: verum

end;

end;