let A1, A2 be Element of Funcs Y,BOOLEAN ; :: thesis: ( ( for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass y,PA & a . x = TRUE ) implies A1 . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass y,PA or not a . x = TRUE ) ) implies A1 . y = FALSE ) ) ) & ( for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass y,PA & a . x = TRUE ) implies A2 . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass y,PA or not a . x = TRUE ) ) implies A2 . y = FALSE ) ) ) implies A1 = A2 )
assume that
A3: for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass y,PA & a . x = TRUE ) implies A1 . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass y,PA or not a . x = TRUE ) ) implies A1 . y = FALSE ) ) and
A4: for y being Element of Y holds
( ( ex x being Element of Y st
( x in EqClass y,PA & a . x = TRUE ) implies A2 . y = TRUE ) & ( ( for x being Element of Y holds
( not x in EqClass y,PA or not a . x = TRUE ) ) implies A2 . y = FALSE ) ) ; :: thesis: A1 = A2
A5: for y being Element of Y holds A1 . y = A2 . y

proof

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

A6: now

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

end;

now

assume A8: for x being Element of Y holds
( not x in EqClass y,PA or not a . x = TRUE ) ; :: thesis: A1 . y = A2 . y
then A2 . y = FALSE by A4;
hence A1 . y = A2 . y by A3, A8; :: thesis: verum

end;

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

end;

consider k3 being Function such that
A9: ( A1 = k3 & dom k3 = Y & rng k3 c= BOOLEAN ) by FUNCT_2:def 2;
consider k4 being Function such that
A10: ( A2 = k4 & dom k4 = Y & rng k4 c= BOOLEAN ) by FUNCT_2:def 2;
for u being set st u in Y holds
k3 . u = k4 . u by A5, A9, A10;
hence A1 = A2 by A9, A10, FUNCT_1:9; :: thesis: verum