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_{1}, b_{2} 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_{1} . x = <.(U_FMT x).] ) & ( for x being Element of the carrier of ET holds b_{2} . x = <.(U_FMT x).] ) holds

b_{1} = b_{2}
; :: thesis: verum

( Y1 . x = <.(U_FMT x).] & ( for y being Element of the carrier of ET holds Y2 . y = <.(U_FMT y).] ) ) ) holds

Y1 = Y2

proof

hence
for b
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

end;( 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

hence
Y1 = Y2
; :: thesis: verum
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;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

b