let f be Function; :: thesis: for A0, D being set st f " D c= A0 holds
f " D = (f | A0) " D
let A0, D be set ; :: thesis: ( f " D c= A0 implies f " D = (f | A0) " D )
assume A1: f " D c= A0 ; :: thesis: f " D = (f | A0) " D
thus (f | A0) " D = (f * (id A0)) " D by RELAT_1:94
.= (id A0) " (f " D) by RELAT_1:181
.= f " D by A1, Th171 ; :: thesis: verum