let f be Function; :: thesis: for A being set holds (f | A) ~ = (f ~) | A
let A be set ; :: thesis: (f | A) ~ = (f ~) | A
A1: dom (f | A) = (dom f) /\ A by RELAT_1:90
.= (dom (f ~)) /\ A by Def1
.= dom ((f ~) | A) by RELAT_1:90 ;

A2: now

let x be set ; :: thesis: ( x in dom ((f ~) | A) implies ((f | A) ~) . x = ((f ~) | A) . x )
assume A3: x in dom ((f ~) | A) ; :: thesis: ((f | A) ~) . x = ((f ~) | A) . x
A4: dom (f | A) c= dom f by RELAT_1:89;

now

per cases ( ex y, z being set st (f | A) . x = [y,z] or for y, z being set holds not (f | A) . x = [y,z] ) ;

suppose ex y, z being set st (f | A) . x = [y,z] ; :: thesis: ((f | A) ~) . x = ((f ~) | A) . x

then consider y, z being set such that
A5: (f | A) . x = [y,z] ;
A6: f . x = [y,z] by A1, A3, A5, FUNCT_1:70;
thus ((f | A) ~) . x = [z,y] by A1, A3, A5, Def1
.= (f ~) . x by A1, A3, A4, A6, Def1
.= ((f ~) | A) . x by A3, FUNCT_1:70 ; :: thesis: verum

end;

suppose A7: for y, z being set holds not (f | A) . x = [y,z] ; :: thesis: ((f | A) ~) . x = ((f ~) | A) . x

A8: (f | A) . x = f . x by A1, A3, FUNCT_1:70;
((f | A) ~) . x = (f | A) . x by A1, A3, A7, Def1;
hence ((f | A) ~) . x = (f ~) . x by A1, A3, A4, A7, A8, Def1
.= ((f ~) | A) . x by A3, FUNCT_1:70 ;
:: thesis: verum

end;

end;

end;

hence ((f | A) ~) . x = ((f ~) | A) . x ; :: thesis: verum

end;

dom ((f | A) ~) = dom (f | A) by Def1;
hence (f | A) ~ = (f ~) | A by A1, A2, FUNCT_1:9; :: thesis: verum