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

now :: thesis: for z being object st z in dom ((A --> x) * h) holds
((A --> x) * h) . z = ((h " A) --> x) . z

let z be object ; :: 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:11;
then A4: h . z in A ;
thus ((A --> x) * h) . z = (A --> x) . (h . z) by A3, FUNCT_1:12
.= x by A4, Th7
.= ((h " A) --> x) . z by A1, A3, Th7 ; :: thesis: verum

end;

hence (A --> x) * h = (h " A) --> x by A1; :: thesis: verum