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

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