let N1, N2 be Binding of OAF; :: thesis: ( ( for i, j being Element of P st i >= j holds
N1 . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i)))) ) & ( for i, j being Element of P st i >= j holds
N2 . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i)))) ) implies N1 = N2 )
assume that
A39: for i, j being Element of P st i >= j holds
N1 . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i)))) and
A40: for i, j being Element of P st i >= j holds
N2 . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i)))) ; :: thesis: N1 = N2

now :: thesis: for ij being object st ij in the InternalRel of P holds
N1 . ij = N2 . ij

let ij be object ; :: thesis: ( ij in the InternalRel of P implies N1 . ij = N2 . ij )
assume A41: ij in the InternalRel of P ; :: thesis: N1 . ij = N2 . ij
then reconsider i2 = ij `1 , i1 = ij `2 as Element of P by MCART_1:10;
reconsider i1 = i1, i2 = i2 as Element of P ;
A42: N2 . ij = N2 . (i2,i1) by A41, MCART_1:21;
ij = [(ij `1),(ij `2)] by A41, MCART_1:21;
then A43: i2 <= i1 by A41, ORDERS_2:def 5;
N1 . ij = N1 . (i2,i1) by A41, MCART_1:21;
then N1 . ij = IFEQ (i2,i1,(id the Sorts of (OAF . i1)),((bind (B,i1,i2)) ** (id the Sorts of (OAF . i1)))) by A39, A43;
hence N1 . ij = N2 . ij by A40, A43, A42; :: thesis: verum

end;

hence N1 = N2 by PBOOLE:3; :: thesis: verum