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)

.= A by A1, Th14

.= dom (A --> (h . x)) ;

hence h * (A --> x) = A --> (h . x) by A2; :: thesis: verum

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

dom (h * (A --> x)) =
(A --> x) " (dom h)
by RELAT_1:147
(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;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

.= A by A1, Th14

.= dom (A --> (h . x)) ;

hence h * (A --> x) = A --> (h . x) by A2; :: thesis: verum