let N1, N2 be Binding of OAF; ( ( 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))))
; N1 = N2
now for ij being object st ij in the InternalRel of P holds
N1 . ij = N2 . ijlet ij be
object ;
( ij in the InternalRel of P implies N1 . ij = N2 . ij )assume A41:
ij in the
InternalRel of
P
;
N1 . ij = N2 . ijthen 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;
verum end;
hence
N1 = N2
by PBOOLE:3; verum