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

consider f being Function such that

A1: ( 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 BinOp of (a . i) ) )

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

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

f . i = pr1 ((a . i),(a . i)) by A1;

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

consider f being Function such that

A1: ( 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 BinOp of (a . i) ) )

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

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

f . i = pr1 ((a . i),(a . i)) by A1;

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