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 Def1;
A2: dom (f | A) = (dom f) /\ A by RELAT_1:90
.= (dom (f ~ )) /\ A by Def1
.= dom ((f ~ ) | A) by RELAT_1:90 ;

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 A2, A3, A5, FUNCT_1:70;
thus ((f | A) ~ ) . x = [z,y] by A2, A3, A5, Def1
.= (f ~ ) . x by A2, 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

then A8: ((f | A) ~ ) . x = (f | A) . x by A2, A3, Def1;
(f | A) . x = f . x by A2, A3, FUNCT_1:70;
hence ((f | A) ~ ) . x = (f ~ ) . x by A2, 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;

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