let X be set ; :: thesis: for f, g being Function st f c= g & X c= dom f holds
f | X = g | X
let f, g be Function; :: thesis: ( f c= g & X c= dom f implies f | X = g | X )
assume that
A1: f c= g and
A2: X c= dom f ; :: thesis: f | X = g | X
thus f | X = (g | (dom f)) | X by A1, Th64
.= g | (X /\ (dom f)) by RELAT_1:100
.= g | X by A2, XBOOLE_1:28 ; :: thesis: verum