let A be non empty 1-sorted ; :: thesis: for B being 1 -element 1-sorted
for t being Point of B
for f being Function of A,B holds f = A --> t
let B be 1 -element 1-sorted ; :: thesis: for t being Point of B
for f being Function of A,B holds f = A --> t
let t be Point of B; :: thesis: for f being Function of A,B holds f = A --> t
let f be Function of A,B; :: thesis: f = A --> t
let a be Element of A; :: according to FUNCT_2:def 8 :: thesis: f . a = (A --> t) . a
thus f . a = (A --> t) . a by STRUCT_0:def 10; :: thesis: verum