deffunc H_{5}( object ) -> Element of bool [:(a . $1),(a . $1):] = id (a . $1);

consider f being Function such that

A2: ( dom f = dom a & ( for x being object st x in dom a holds

f . x = H_{5}(x) ) )
from FUNCT_1:sch 3();

take f ; :: thesis: ( dom f = dom a & ( for i being Element of dom a holds f . i is UnOp of (a . i) ) )

thus dom f = dom a by A2; :: thesis: for i being Element of dom a holds f . i is UnOp of (a . i)

let i be Element of dom a; :: thesis: f . i is UnOp of (a . i)

f . i = id (a . i) by A2;

hence f . i is UnOp of (a . i) ; :: thesis: verum

consider f being Function such that

A2: ( dom f = dom a & ( for x being object st x in dom a holds

f . x = H

take f ; :: thesis: ( dom f = dom a & ( for i being Element of dom a holds f . i is UnOp of (a . i) ) )

thus dom f = dom a by A2; :: thesis: for i being Element of dom a holds f . i is UnOp of (a . i)

let i be Element of dom a; :: thesis: f . i is UnOp of (a . i)

f . i = id (a . i) by A2;

hence f . i is UnOp of (a . i) ; :: thesis: verum