let F1, F2 be Function of (Sub U0),(bool the carrier of U0); :: thesis: ( ( for u being Element of Sub U0 holds F1 . u = carr u ) & ( for u being Element of Sub U0 holds F2 . u = carr u ) implies F1 = F2 )
assume that
A1: for u1 being Element of Sub U0 holds F1 . u1 = carr u1 and
A2: for u2 being Element of Sub U0 holds F2 . u2 = carr u2 ; :: thesis: F1 = F2
for u being object st u in Sub U0 holds
F1 . u = F2 . u

proof

let u be object ; :: thesis: ( u in Sub U0 implies F1 . u = F2 . u )
assume u in Sub U0 ; :: thesis: F1 . u = F2 . u
then reconsider u1 = u as Element of Sub U0 ;
consider U1 being SubAlgebra of U0 such that
u1 = U1 and
A3: carr u1 = the carrier of U1 by Def2;
F1 . u1 = the carrier of U1 by A1, A3;
hence F1 . u = F2 . u by A2, A3; :: thesis: verum

end;

hence F1 = F2 by FUNCT_2:12; :: thesis: verum