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 ;

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

hence
(A --> x) * h = (h " A) --> x
by A1; :: thesis: verum((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;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