let h be Function; :: thesis: for A being set
for x being object st x in dom h holds
h * (A --> x) = A --> (h . x)
let A be set ; :: thesis: for x being object st x in dom h holds
h * (A --> x) = A --> (h . x)
let x be object ; :: thesis: ( x in dom h implies h * (A --> x) = A --> (h . x) )
assume A1: x in dom h ; :: thesis: h * (A --> x) = A --> (h . x)

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

let z be object ; :: thesis: ( z in dom (h * (A --> x)) implies (h * (A --> x)) . z = (A --> (h . x)) . z )
assume A3: z in dom (h * (A --> x)) ; :: thesis: (h * (A --> x)) . z = (A --> (h . x)) . z
then z in dom (A --> x) by FUNCT_1:11;
then A4: z in A ;
thus (h * (A --> x)) . z = h . ((A --> x) . z) by A3, FUNCT_1:12
.= h . x by A4, Th7
.= (A --> (h . x)) . z by A4, Th7 ; :: thesis: verum

end;

dom (h * (A --> x)) = (A --> x) " (dom h) by RELAT_1:147
.= A by A1, Th14
.= dom (A --> (h . x)) ;
hence h * (A --> x) = A --> (h . x) by A2; :: thesis: verum