A1: dom (x .--> y) = {x} ;
rng (x .--> y) = {y} by FUNCOP_1:8;
then reconsider R = x .--> y as Relation of {x},(bool {x}) by A1, RELSET_1:4;
R is quasi_total by A1, FUNCT_2:def 1;
hence x .--> y is Function of {x},(bool {x}) ; :: thesis: verum