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 )
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 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;
assume A3: for u being Element of Sub U0
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
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;
hence f = Carr U0 by Def3; :: thesis: verum