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) . {$1} & A = (ObjectDerivation C) . ((AttributeDerivation 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) . ((AttributeDerivation C) . se);
set O = (AttributeDerivation C) . se;
take ConceptStr(# ((AttributeDerivation C) . se),((ObjectDerivation C) . ((AttributeDerivation C) . se)) #) ; :: thesis: ( ConceptStr(# ((AttributeDerivation C) . se),((ObjectDerivation C) . ((AttributeDerivation C) . se)) #) in the carrier of (ConceptLattice C) & S₁[e, ConceptStr(# ((AttributeDerivation C) . se),((ObjectDerivation C) . ((AttributeDerivation C) . se)) #)] )
( ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #) & ConceptStr(# ((AttributeDerivation C) . se),((ObjectDerivation C) . ((AttributeDerivation C) . se)) #) is FormalConcept of C ) by CONLAT_1:21, CONLAT_1:def 20;
hence ( ConceptStr(# ((AttributeDerivation C) . se),((ObjectDerivation C) . ((AttributeDerivation C) . se)) #) in the carrier of (ConceptLattice C) & S₁[e, ConceptStr(# ((AttributeDerivation C) . se),((ObjectDerivation C) . ((AttributeDerivation 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 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
( f . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) )
let o be Element of the carrier' 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) . {o} & A = (ObjectDerivation C) . ((AttributeDerivation 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) . {o} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {o}) ) by A2; :: thesis: verum