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 = (AttributeDerivation C) . ((ObjectDerivation C) . (the Extent of CP1 \/ the Extent of CP2)) & A = 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 = (AttributeDerivation C) . ((ObjectDerivation C) . (the Extent of CP1 \/ the Extent of CP2)) & A = the Intent of CP1 /\ the Intent of CP2 ) ) implies F1 = F2 )
assume A4: 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 = (AttributeDerivation C) . ((ObjectDerivation C) . (the Extent of CP1 \/ the Extent of CP2)) & A = 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 = (AttributeDerivation C) . ((ObjectDerivation C) . (the Extent of CP1 \/ the Extent of CP2)) or not A = the Intent of CP1 /\ the Intent of CP2 ) or 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
( F2 . CP1,CP2 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . (the Extent of CP1 \/ the Extent of CP2)) & A = the Intent of CP1 /\ the Intent of CP2 ) ; :: thesis: F1 = F2
A6: 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
A7: A in B-carrier C and
A8: B in B-carrier C and
A9: X = [A,B] by ZFMISC_1:def 2;
reconsider B = B as strict FormalConcept of C by A8, Th35;
reconsider A = A as strict FormalConcept of C by A7, Th35;
( 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 = (AttributeDerivation C) . ((ObjectDerivation C) . (the Extent of A \/ the Extent of B)) & At = 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 = (AttributeDerivation C) . ((ObjectDerivation C) . (the Extent of A \/ the Extent of B)) & At9 = the Intent of A /\ the Intent of B ) ) by A4, A5;
hence F1 . X = F2 . X by A9; :: 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 A6, FUNCT_1:9; :: thesis: verum