let F1, F2 be Function of the carrier' of C, the carrier of (ConceptLattice C); :: thesis: ( ( for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( F1 . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) ) & ( for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( F2 . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) ) implies F1 = F2 )
assume A3: for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( F1 . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) ; :: thesis: ( ex a being Element of the carrier' of C st
for O being Subset of the carrier of C
for A being Subset of the carrier' of C holds
( not F2 . a = ConceptStr(# O,A #) or not O = (AttributeDerivation C) . {a} or not A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) or F1 = F2 )
assume A4: for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( F2 . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) ; :: thesis: F1 = F2
A5: for a being object st a in the carrier' of C holds
F1 . a = F2 . a

proof

let a be object ; :: thesis: ( a in the carrier' of C implies F1 . a = F2 . a )
assume a in the carrier' of C ; :: thesis: F1 . a = F2 . a
then reconsider a = a as Element of the carrier' of C ;
( ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( F1 . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) & ex O9 being Subset of the carrier of C ex A9 being Subset of the carrier' of C st
( F2 . a = ConceptStr(# O9,A9 #) & O9 = (AttributeDerivation C) . {a} & A9 = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) ) by A3, A4;
hence F1 . a = F2 . a ; :: thesis: verum

end;

( dom F1 = the carrier' of C & dom F2 = the carrier' of C ) by FUNCT_2:def 1;
hence F1 = F2 by A5; :: thesis: verum