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

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