let h be Function; :: thesis: for A, x being set holds (A --> x) * h = (h " A) --> x
let A, x be set ; :: thesis: (A --> x) * h = (h " A) --> x
A1: dom ((A --> x) * h) = h " (dom (A --> x)) by RELAT_1:182
.= h " A by Th19 ;

A2: now

let z be set ; :: thesis: ( z in dom ((A --> x) * h) implies ((A --> x) * h) . z = ((h " A) --> x) . z )
assume A3: z in dom ((A --> x) * h) ; :: thesis: ((A --> x) * h) . z = ((h " A) --> x) . z
then h . z in dom (A --> x) by FUNCT_1:21;
then A4: h . z in A by Th19;
thus ((A --> x) * h) . z = (A --> x) . (h . z) by A3, FUNCT_1:22
.= x by A4, Th13
.= ((h " A) --> x) . z by A1, A3, Th13 ; :: thesis: verum

end;

dom ((A --> x) * h) = dom ((h " A) --> x) by A1, Th19;
hence (A --> x) * h = (h " A) --> x by A2, FUNCT_1:9; :: thesis: verum