let I, x be set ; :: thesis: for C being Category
for a being Object of C
for F being Projections_family of a,I st x in I holds
dom (F /. x) = a
let C be Category; :: thesis: for a being Object of C
for F being Projections_family of a,I st x in I holds
dom (F /. x) = a
let a be Object of C; :: thesis: for F being Projections_family of a,I st x in I holds
dom (F /. x) = a
let F be Projections_family of a,I; :: thesis: ( x in I implies dom (F /. x) = a )
assume A1: x in I ; :: thesis: dom (F /. x) = a
(doms F) /. x = (I --> a) /. x by Def13;
hence dom (F /. x) = (I --> a) /. x by A1, Def1
.= a by A1, Th2 ;
:: thesis: verum