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 ;
ij = [(ij `1),(ij `2)] by ;
then A43: i2 <= i1 by ;
N1 . ij = N1 . (i2,i1) by ;
then N1 . ij = IFEQ (i2,i1,(id the Sorts of (OAF . i1)),((bind (B,i1,i2)) ** (id the Sorts of (OAF . i1)))) by ;
hence N1 . ij = N2 . ij by ; :: thesis: verum
end;
hence N1 = N2 by PBOOLE:3; :: thesis: verum