let f, g be Function of P,Q; :: thesis: ( ( for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
f . p = sup M ) & ( for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
g . p = sup M ) implies f = g )
( ( for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
f . p = sup M ) & ( for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
g . p = sup M ) implies f = g )

proof

assume C1: ( ( for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
f . p = sup M ) & ( for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
g . p = sup M ) ) ; :: thesis: f = g
set X = the carrier of P;
set Y = the carrier of Q;
for x being set st x in the carrier of P holds
f . x = g . x

proof

let x be set ; :: thesis: ( x in the carrier of P implies f . x = g . x )
assume x in the carrier of P ; :: thesis: f . x = g . x
then reconsider p = x as Element of P ;
reconsider M = F -image p as non empty Chain of Q ;
f . x = sup M by C1
.= g . x by C1 ;
hence f . x = g . x ; :: thesis: verum

end;

hence f = g by FUNCT_2:18; :: thesis: verum

end;

hence ( ( for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
f . p = sup M ) & ( for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
g . p = sup M ) implies f = g ) ; :: thesis: verum