defpred S₁[ object , object ] means ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( $2 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {$1}) & A = (ObjectDerivation C) . {$1} );
A1: for e being object st e in the carrier of C holds
ex u being object st
( u in the carrier of (ConceptLattice C) & S₁[e,u] )

proof

let e be object ; :: thesis: ( e in the carrier of C implies ex u being object st
( u in the carrier of (ConceptLattice C) & S₁[e,u] ) )
assume e in the carrier of C ; :: thesis: ex u being object st
( u in the carrier of (ConceptLattice C) & S₁[e,u] )
then reconsider se = {e} as Subset of the carrier of C by ZFMISC_1:31;
set A = (ObjectDerivation C) . se;
set O = (AttributeDerivation C) . ((ObjectDerivation C) . se);
take ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . se)),((ObjectDerivation C) . se) #) ; :: thesis: ( ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . se)),((ObjectDerivation C) . se) #) in the carrier of (ConceptLattice C) & S₁[e, ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . se)),((ObjectDerivation C) . se) #)] )
( ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #) & ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . se)),((ObjectDerivation C) . se) #) is FormalConcept of C ) by CONLAT_1:19, CONLAT_1:def 20;
hence ( ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . se)),((ObjectDerivation C) . se) #) in the carrier of (ConceptLattice C) & S₁[e, ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . se)),((ObjectDerivation C) . se) #)] ) by CONLAT_1:31; :: thesis: verum

end;

consider f being Function of the carrier of C, the carrier of (ConceptLattice C) such that
A2: for e being object st e in the carrier of C holds
S₁[e,f . e] from FUNCT_2:sch 1(A1);
take f ; :: 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
( f . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} )
let o be Element of C; :: thesis: ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( f . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} )
thus ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( f . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) by A2; :: thesis: verum