let f, g, h be Function; :: thesis: ( f c= g & f c= h implies g | (dom f) = h | (dom f) )
assume that
A1: f c= g and
A2: f c= h ; :: thesis: g | (dom f) = h | (dom f)
thus g | (dom f) = f by A1, Th21
.= h | (dom f) by A2, Th21 ; :: thesis: verum