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 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)) ) ; :: 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 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)) ) ; :: thesis: 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 ; :: 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 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; :: thesis: 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; :: thesis: verum