let F1, F2 be BinOp of (B-carrier C); ( ( for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( F1 . (CP1,CP2) = ConceptStr(# O,A #) & O = the Extent of CP1 /\ the Extent of CP2 & A = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2)) ) ) & ( for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( F2 . (CP1,CP2) = ConceptStr(# O,A #) & O = the Extent of CP1 /\ the Extent of CP2 & A = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2)) ) ) implies F1 = F2 )
assume A5:
for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( F1 . (CP1,CP2) = ConceptStr(# O,A #) & O = the Extent of CP1 /\ the Extent of CP2 & A = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2)) )
; ( ex CP1, CP2 being strict FormalConcept of C st
for O being Subset of the carrier of C
for A being Subset of the carrier' of C holds
( not F2 . (CP1,CP2) = ConceptStr(# O,A #) or not O = the Extent of CP1 /\ the Extent of CP2 or not A = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2)) ) or F1 = F2 )
assume A6:
for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( F2 . (CP1,CP2) = ConceptStr(# O,A #) & O = the Extent of CP1 /\ the Extent of CP2 & A = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2)) )
; F1 = F2
A7:
for X being object st X in [:(B-carrier C),(B-carrier C):] holds
F1 . X = F2 . X
proof
let X be
object ;
( X in [:(B-carrier C),(B-carrier C):] implies F1 . X = F2 . X )
assume
X in [:(B-carrier C),(B-carrier C):]
;
F1 . X = F2 . X
then consider A,
B being
object such that A8:
A in B-carrier C
and A9:
B in B-carrier C
and A10:
X = [A,B]
by ZFMISC_1:def 2;
reconsider B =
B as
strict FormalConcept of
C by A9, Th31;
reconsider A =
A as
strict FormalConcept of
C by A8, Th31;
( ex
O being
Subset of the
carrier of
C ex
At being
Subset of the
carrier' of
C st
(
F1 . (
A,
B)
= ConceptStr(#
O,
At #) &
O = the
Extent of
A /\ the
Extent of
B &
At = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of A \/ the Intent of B)) ) & ex
O9 being
Subset of the
carrier of
C ex
At9 being
Subset of the
carrier' of
C st
(
F2 . (
A,
B)
= ConceptStr(#
O9,
At9 #) &
O9 = the
Extent of
A /\ the
Extent of
B &
At9 = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of A \/ the Intent of B)) ) )
by A5, A6;
hence
F1 . X = F2 . X
by A10;
verum
end;
( dom F1 = [:(B-carrier C),(B-carrier C):] & dom F2 = [:(B-carrier C),(B-carrier C):] )
by FUNCT_2:def 1;
hence
F1 = F2
by A7, FUNCT_1:2; verum