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
A38: 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
A39: 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

let ij be set ; :: thesis: ( ij in the InternalRel of P implies N1 . ij = N2 . ij )
assume A40: 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 ;
A41: N2 . ij = N2 . (i2,i1) by A40, MCART_1:21;
ij = [(ij `1),(ij `2)] by A40, MCART_1:21;
then A42: i2 <= i1 by A40, ORDERS_2:def 5;
N1 . ij = N1 . (i2,i1) by A40, 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 A38, A42;
hence N1 . ij = N2 . ij by A39, A42, A41; :: thesis: verum

end;

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