let x, y, z, A be set ; :: thesis: ( z in A implies (A --> x) * (y .--> z) = y .--> x )
assume A1: z in A ; :: thesis: (A --> x) * (y .--> z) = y .--> x
A2: dom (y .--> z) = {y}
.= dom (y .--> x) ;
rng (y .--> z) = {z} by Th88;
then rng (y .--> z) c= dom (A --> x) by A1, ZFMISC_1:31;
hence dom ((A --> x) * (y .--> z)) = dom (y .--> x) by A2, RELAT_1:27; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in proj1 ((A --> x) * (y .--> z)) or ((A --> x) * (y .--> z)) . b₁ = (y .--> x) . b₁ )
let e be object ; :: thesis: ( not e in proj1 ((A --> x) * (y .--> z)) or ((A --> x) * (y .--> z)) . e = (y .--> x) . e )
assume A3: e in dom ((A --> x) * (y .--> z)) ; :: thesis: ((A --> x) * (y .--> z)) . e = (y .--> x) . e
thus ((A --> x) * (y .--> z)) . e = (A --> x) . ((y .--> z) . e) by A3, FUNCT_1:12
.= (A --> x) . z by A3, Th7
.= x by A1, Th7
.= (y .--> x) . e by A3, Th7 ; :: thesis: verum