let F1, F2 be Function of the carrier of C, the carrier of (ConceptLattice C); :: thesis: ( ( for o being Element 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 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 A3: for o being Element 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 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 A4: for o being Element 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
A5: for o being object st o in the carrier of C holds
F1 . o = F2 . o
proof
let o be object ; :: 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 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} ) & ex O9 being Subset of the carrier of C ex A9 being Subset of the carrier' of C st
( F2 . o = ConceptStr(# O9,A9 #) & O9 = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A9 = (ObjectDerivation C) . {o} ) ) by A3, A4;
hence F1 . o = F2 . o ; :: 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