let y be set ; :: thesis: for C being Category
for a being Object of C
for f being Morphism of C st dom f = a holds
y .--> f is Projections_family of a,{y}

let C be Category; :: thesis: for a being Object of C
for f being Morphism of C st dom f = a holds
y .--> f is Projections_family of a,{y}

let a be Object of C; :: thesis: for f being Morphism of C st dom f = a holds
y .--> f is Projections_family of a,{y}

let f be Morphism of C; :: thesis: ( dom f = a implies y .--> f is Projections_family of a,{y} )
set F = y .--> f;
assume A1: dom f = a ; :: thesis: y .--> f is Projections_family of a,{y}
now :: thesis: for x being set st x in {y} holds
(doms (y .--> f)) /. x = (y .--> a) /. x
let x be set ; :: thesis: ( x in {y} implies (doms (y .--> f)) /. x = (y .--> a) /. x )
assume A2: x in {y} ; :: thesis: (doms (y .--> f)) /. x = (y .--> a) /. x
hence (doms (y .--> f)) /. x = dom ((y .--> f) /. x) by Def1
.= a by A1, A2, Th2
.= (y .--> a) /. x by ;
:: thesis: verum
end;
hence doms (y .--> f) = {y} --> a by Th1; :: according to CAT_3:def 13 :: thesis: verum