let A1, A2 be Element of Funcs Y,BOOLEAN ; :: thesis: ( ( for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass y,PA holds
a . x = TRUE ) implies A1 . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass y,PA & not a . x = TRUE ) implies A1 . y = FALSE ) ) ) & ( for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass y,PA holds
a . x = TRUE ) implies A2 . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass y,PA & not a . x = TRUE ) implies A2 . y = FALSE ) ) ) implies A1 = A2 )
assume that
A3: for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass y,PA holds
a . x = TRUE ) implies A1 . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass y,PA & not a . x = TRUE ) implies A1 . y = FALSE ) ) and
A4: for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass y,PA holds
a . x = TRUE ) implies A2 . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass y,PA & not a . x = TRUE ) implies A2 . y = FALSE ) ) ; :: thesis: A1 = A2
consider k4 being Function such that
A5: A2 = k4 and
A6: dom k4 = Y and
rng k4 c= BOOLEAN by FUNCT_2:def 2;
consider k3 being Function such that
A7: A1 = k3 and
A8: dom k3 = Y and
rng k3 c= BOOLEAN by FUNCT_2:def 2;
for y being Element of Y holds A1 . y = A2 . y

proof

let y be Element of Y; :: thesis: A1 . y = A2 . y

A9: now

assume A10: ex x being Element of Y st
( x in EqClass y,PA & not a . x = TRUE ) ; :: thesis: A1 . y = A2 . y
then A2 . y = FALSE by A4;
hence A1 . y = A2 . y by A3, A10; :: thesis: verum

end;

now

assume A11: for x being Element of Y st x in EqClass y,PA holds
a . x = TRUE ; :: thesis: A1 . y = A2 . y
then A2 . y = TRUE by A4;
hence A1 . y = A2 . y by A3, A11; :: thesis: verum

end;

hence A1 . y = A2 . y by A9; :: thesis: verum

end;

then for u being set st u in Y holds
k3 . u = k4 . u by A7, A5;
hence A1 = A2 by A7, A8, A5, A6, FUNCT_1:9; :: thesis: verum