let h be Function; :: thesis: for A, x being set st x in dom h holds
h * (A --> x) = A --> (h . x)
let A, x be set ; :: 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

let z be set ; :: 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:21;
then A4: z in A by Th19;
thus (h * (A --> x)) . z = h . ((A --> x) . z) by A3, FUNCT_1:22
.= h . x by A4, Th13
.= (A --> (h . x)) . z by A4, Th13 ; :: thesis: verum

end;

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