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
A33:
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
A34:
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 A35:
ij in the
InternalRel of
P
;
:: thesis: 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 ;
ij = [(ij `1 ),(ij `2 )]
by A35, MCART_1:23;
then A36:
i2 <= i1
by A35, ORDERS_2:def 9;
N1 . ij = N1 . i2,
i1
by A35, MCART_1:23;
then A37:
N1 . ij = IFEQ i2,
i1,
(id the Sorts of (OAF . i1)),
((bind B,i1,i2) ** (id the Sorts of (OAF . i1)))
by A33, A36;
N2 . ij = N2 . i2,
i1
by A35, MCART_1:23;
hence
N1 . ij = N2 . ij
by A34, A36, A37;
:: thesis: verum end;
hence
N1 = N2
by PBOOLE:3; :: thesis: verum