let F1, F2 be BinOp of (B-carrier C); :: thesis: ( ( 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 A7: 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)) ) ; :: thesis: ( 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 A8: 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)) ) ; :: thesis: F1 = F2
A9: for X being set st X in [:(B-carrier C),(B-carrier C):] holds
F1 . X = F2 . X

proof

let X be set ; :: thesis: ( X in [:(B-carrier C),(B-carrier C):] implies F1 . X = F2 . X )
assume X in [:(B-carrier C),(B-carrier C):] ; :: thesis: F1 . X = F2 . X
then consider A, B being set such that
A10: ( A in B-carrier C & B in B-carrier C & X = [A,B] ) by ZFMISC_1:def 2;
reconsider A = A as strict FormalConcept of C by A10, Th35;
reconsider B = B as strict FormalConcept of C by A10, Th35;
consider O being Subset of the carrier of C, At being Subset of the carrier' of C such that
A11: ( 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)) ) by A7;
consider O' being Subset of the carrier of C, At' being Subset of the carrier' of C such that
A12: ( F2 . 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)) ) by A8;
thus F1 . X = F2 . X by A10, A11, A12; :: thesis: verum

end;

A13: dom F1 = [:(B-carrier C),(B-carrier C):] by FUNCT_2:def 1;
dom F2 = [:(B-carrier C),(B-carrier C):] by FUNCT_2:def 1;
hence F1 = F2 by A9, A13, FUNCT_1:9; :: thesis: verum