let F1, F2 be Function of the carrier of C,the carrier of (ConceptLattice C); :: thesis: ( ( for o 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 . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) ) & ( for o 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 . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) ) implies F1 = F2 )
assume A4: for o 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 . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) ; :: thesis: ( ex o 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 . o = ConceptStr(# O,A #) or not O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) or not A = (ObjectDerivation C) . {o} ) or F1 = F2 )
assume A5: for o 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 . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) ; :: thesis: F1 = F2
A6: for o being set st o in the carrier of C holds
F1 . o = F2 . o

proof

let o be set ; :: thesis: ( o in the carrier of C implies F1 . o = F2 . o )
assume o in the carrier of C ; :: thesis: F1 . o = F2 . o
then reconsider o = o as Element of the carrier of C ;
consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that
A7: ( F1 . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) by A4;
consider O' being Subset of the carrier of C, A' being Subset of the carrier' of C such that
A8: ( F2 . o = ConceptStr(# O',A' #) & O' = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A' = (ObjectDerivation C) . {o} ) by A5;
thus F1 . o = F2 . o by A7, A8; :: thesis: verum

end;

A9: dom F1 = the carrier of C by FUNCT_2:def 1;
dom F2 = the carrier of C by FUNCT_2:def 1;
hence F1 = F2 by A6, A9, FUNCT_1:9; :: thesis: verum