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

A2: now :: thesis: for x being object st x in dom ((f ~) | A) holds
((f | A) ~) . x = ((f ~) | A) . x

let x be object ; :: 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:60;

now :: thesis: ((f | A) ~) . x = ((f ~) | A) . x

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

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

then consider y, z being object such that
A5: (f | A) . x = [y,z] ;
A6: f . x = [y,z] by A1, A3, A5, FUNCT_1:47;
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:47 ; :: thesis: verum

end;

suppose A7: for y, z being object 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:47;
((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:47 ;
:: 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; :: thesis: verum