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

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

hence
F1 = F2
by FUNCT_2:12; :: thesis: verum
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;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