let f be Function of (Sub U0),(bool the carrier of U0); :: thesis: ( f = Carr U0 iff for u being Element of Sub U0

for U1 being SubAlgebra of U0 st u = U1 holds

f . u = the carrier of U1 )

for U1 being SubAlgebra of U0 st u = U1 holds

f . u = the carrier of U1 ; :: thesis: f = Carr U0

for u1 being Element of Sub U0 holds f . u1 = carr u1

for U1 being SubAlgebra of U0 st u = U1 holds

f . u = the carrier of U1 )

hereby :: thesis: ( ( for u being Element of Sub U0

for U1 being SubAlgebra of U0 st u = U1 holds

f . u = the carrier of U1 ) implies f = Carr U0 )

assume A3:
for u being Element of Sub U0for U1 being SubAlgebra of U0 st u = U1 holds

f . u = the carrier of U1 ) implies f = Carr U0 )

assume A1:
f = Carr U0
; :: thesis: for u being Element of Sub U0

for U1 being SubAlgebra of U0 st u = U1 holds

f . u = the carrier of U1

let u be Element of Sub U0; :: thesis: for U1 being SubAlgebra of U0 st u = U1 holds

f . u = the carrier of U1

let U1 be SubAlgebra of U0; :: thesis: ( u = U1 implies f . u = the carrier of U1 )

assume A2: u = U1 ; :: thesis: f . u = the carrier of U1

ex U2 being SubAlgebra of U0 st

( u = U2 & carr u = the carrier of U2 ) by Def2;

hence f . u = the carrier of U1 by A1, A2, Def3; :: thesis: verum

end;for U1 being SubAlgebra of U0 st u = U1 holds

f . u = the carrier of U1

let u be Element of Sub U0; :: thesis: for U1 being SubAlgebra of U0 st u = U1 holds

f . u = the carrier of U1

let U1 be SubAlgebra of U0; :: thesis: ( u = U1 implies f . u = the carrier of U1 )

assume A2: u = U1 ; :: thesis: f . u = the carrier of U1

ex U2 being SubAlgebra of U0 st

( u = U2 & carr u = the carrier of U2 ) by Def2;

hence f . u = the carrier of U1 by A1, A2, Def3; :: thesis: verum

for U1 being SubAlgebra of U0 st u = U1 holds

f . u = the carrier of U1 ; :: thesis: f = Carr U0

for u1 being Element of Sub U0 holds f . u1 = carr u1

proof

hence
f = Carr U0
by Def3; :: thesis: verum
let u be Element of Sub U0; :: thesis: f . u = carr u

reconsider U1 = u as Element of Sub U0 ;

f . u = the carrier of U1 by A3;

hence f . u = carr u by Def2; :: thesis: verum

end;reconsider U1 = u as Element of Sub U0 ;

f . u = the carrier of U1 by A3;

hence f . u = carr u by Def2; :: thesis: verum