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

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

hence
N1 = N2
by PBOOLE:3; :: thesis: verumN1 . 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;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