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

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