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 = <.(U_FMT x).] & ( for y being Element of the carrier of ET holds Y2 . y = <.(U_FMT 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 = <.(U_FMT x).] & ( for y being Element of the carrier of ET holds Y2 . y = <.(U_FMT y).] ) ) ) implies Y1 = Y2 )
assume A2: for x being Element of the carrier of ET holds
( Y1 . x = <.(U_FMT x).] & ( for y being Element of the carrier of ET holds Y2 . y = <.(U_FMT 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 = <.(U_FMT t).] & Y2 . t = <.(U_FMT t).] ) by A2;
hence Y1 . t = Y2 . t ; :: thesis: verum

end;

hence Y1 = Y2 ; :: thesis: verum

end;

hence for b₁, b₂ being Function of the carrier of ET,(bool (bool the carrier of ET)) st ( for x being Element of the carrier of ET holds b₁ . x = <.(U_FMT x).] ) & ( for x being Element of the carrier of ET holds b₂ . x = <.(U_FMT x).] ) holds
b₁ = b₂ ; :: thesis: verum