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:23;
ij = [(ij `1 ),(ij `2 )] by A40, MCART_1:23;
then A42: i2 <= i1 by A40, ORDERS_2:def 9;
N1 . ij = N1 . i2,i1 by A40, MCART_1:23;
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