let A1, A2 be Function of 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
let y be Element of Y; :: according to FUNCT_2:def 8 :: thesis: A1 . y = A2 . y

A5: now :: thesis: ( ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) implies A1 . y = A2 . y )

assume A6: 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, A6; :: thesis: verum

end;

now :: thesis: ( ( for x being Element of Y st x in EqClass (y,PA) holds
a . x = TRUE ) implies A1 . y = A2 . y )

assume A7: 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, A7; :: thesis: verum

end;

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