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}

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

hence
doms (y .--> f) = {y} --> a
by Th1; :: according to CAT_3:def 13 :: thesis: verum(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 A2, Th2 ;

:: thesis: verum

end;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 A2, Th2 ;

:: thesis: verum