for Y1, Y2 being Function of the carrier of ET,(bool (bool the carrier of ET)) st ( for x being Element of the carrier of ET holds
( Y1 . x = <.().] & ( for y being Element of the carrier of ET holds Y2 . y = <.().] ) ) ) holds
Y1 = Y2
proof
let Y1, Y2 be Function of the carrier of ET,(bool (bool the carrier of ET)); :: thesis: ( ( for x being Element of the carrier of ET holds
( Y1 . x = <.().] & ( for y being Element of the carrier of ET holds Y2 . y = <.().] ) ) ) implies Y1 = Y2 )

assume A2: for x being Element of the carrier of ET holds
( Y1 . x = <.().] & ( for y being Element of the carrier of ET holds Y2 . y = <.().] ) ) ; :: thesis: Y1 = Y2
for t being object st t in the carrier of ET holds
Y1 . t = Y2 . t
proof
let t be object ; :: thesis: ( t in the carrier of ET implies Y1 . t = Y2 . t )
assume A3: t in the carrier of ET ; :: thesis: Y1 . t = Y2 . t
reconsider t = t as Element of the carrier of ET by A3;
( Y1 . t = <.().] & Y2 . t = <.().] ) by A2;
hence Y1 . t = Y2 . t ; :: thesis: verum
end;
hence Y1 = Y2 ; :: thesis: verum
end;
hence for b1, b2 being Function of the carrier of ET,(bool (bool the carrier of ET)) st ( for x being Element of the carrier of ET holds b1 . x = <.().] ) & ( for x being Element of the carrier of ET holds b2 . x = <.().] ) holds
b1 = b2 ; :: thesis: verum