let I, x be set ; :: thesis: for A being non empty set
for a being Element of A st x in I holds
(I --> a) /. x = a
let A be non empty set ; :: thesis: for a being Element of A st x in I holds
(I --> a) /. x = a
let a be Element of A; :: thesis: ( x in I implies (I --> a) /. x = a )
assume A1: x in I ; :: thesis: (I --> a) /. x = a
hence a = (I --> a) . x by FUNCOP_1:7
.= (I --> a) /. x by A1, FUNCT_2:def 13 ;
:: thesis: verum