let f be Function; :: thesis: for A0, C being set st C c= A0 holds
f .: C = (f | A0) .: C
let A0, C be set ; :: thesis: ( C c= A0 implies f .: C = (f | A0) .: C )
assume A1: C c= A0 ; :: thesis: f .: C = (f | A0) .: C
thus (f | A0) .: C = (f * (id A0)) .: C by RELAT_1:65
.= f .: ((id A0) .: C) by RELAT_1:126
.= f .: C by A1, FUNCT_1:92 ; :: thesis: verum