let M1, M2 be ManySortedSet of [:I,I,I:]; :: thesis: ( ( for i, j, k being object st i in I & j in I & k in I holds

M1 . (i,j,k) = G . (i,k) ) & ( for i, j, k being object st i in I & j in I & k in I holds

M2 . (i,j,k) = G . (i,k) ) implies M1 = M2 )

assume that

A2: for i, j, k being object st i in I & j in I & k in I holds

M1 . (i,j,k) = G . (i,k) and

A3: for i, j, k being object st i in I & j in I & k in I holds

M2 . (i,j,k) = G . (i,k) ; :: thesis: M1 = M2

M1 . (i,j,k) = G . (i,k) ) & ( for i, j, k being object st i in I & j in I & k in I holds

M2 . (i,j,k) = G . (i,k) ) implies M1 = M2 )

assume that

A2: for i, j, k being object st i in I & j in I & k in I holds

M1 . (i,j,k) = G . (i,k) and

A3: for i, j, k being object st i in I & j in I & k in I holds

M2 . (i,j,k) = G . (i,k) ; :: thesis: M1 = M2

now :: thesis: for i, j, k being object st i in I & j in I & k in I holds

M1 . (i,j,k) = M2 . (i,j,k)

hence
M1 = M2
by Th4; :: thesis: verumM1 . (i,j,k) = M2 . (i,j,k)

let i, j, k be object ; :: thesis: ( i in I & j in I & k in I implies M1 . (i,j,k) = M2 . (i,j,k) )

assume A4: ( i in I & j in I & k in I ) ; :: thesis: M1 . (i,j,k) = M2 . (i,j,k)

hence M1 . (i,j,k) = G . (i,k) by A2

.= M2 . (i,j,k) by A3, A4 ;

:: thesis: verum

end;assume A4: ( i in I & j in I & k in I ) ; :: thesis: M1 . (i,j,k) = M2 . (i,j,k)

hence M1 . (i,j,k) = G . (i,k) by A2

.= M2 . (i,j,k) by A3, A4 ;

:: thesis: verum