let X be set ; :: thesis: for f, g being Function st X c= dom f & f c= g holds
f | X = g | X
let f, g be Function; :: thesis: ( X c= dom f & f c= g implies f | X = g | X )
assume A1: X c= dom f ; :: thesis: ( not f c= g or f | X = g | X )
assume f c= g ; :: thesis: f | X = g | X
hence f | X = (g | (dom f)) | X by Th21
.= g | ((dom f) /\ X) by RELAT_1:71
.= g | X by A1, XBOOLE_1:28 ;
:: thesis: verum