take U1 = U0; :: thesis: ( the carrier of U1 is Subset of U0 & ( for B being non empty Subset of U0 st B = the carrier of U1 holds

( the charact of U1 = Opers (U0,B) & B is opers_closed ) ) )

A1: for B being non empty Subset of U0 st B = the carrier of U0 holds

( the charact of U0 = Opers (U0,B) & B is opers_closed )

hence ( the carrier of U1 is Subset of U0 & ( for B being non empty Subset of U0 st B = the carrier of U1 holds

( the charact of U1 = Opers (U0,B) & B is opers_closed ) ) ) by A1; :: thesis: verum

( the charact of U1 = Opers (U0,B) & B is opers_closed ) ) )

A1: for B being non empty Subset of U0 st B = the carrier of U0 holds

( the charact of U0 = Opers (U0,B) & B is opers_closed )

proof

the carrier of U1 c= the carrier of U1
;
let B be non empty Subset of U0; :: thesis: ( B = the carrier of U0 implies ( the charact of U0 = Opers (U0,B) & B is opers_closed ) )

assume A2: B = the carrier of U0 ; :: thesis: ( the charact of U0 = Opers (U0,B) & B is opers_closed )

A3: dom the charact of U0 = dom (Opers (U0,B)) by Def6;

for n being Nat st n in dom the charact of U0 holds

the charact of U0 . n = (Opers (U0,B)) . n

end;assume A2: B = the carrier of U0 ; :: thesis: ( the charact of U0 = Opers (U0,B) & B is opers_closed )

A3: dom the charact of U0 = dom (Opers (U0,B)) by Def6;

for n being Nat st n in dom the charact of U0 holds

the charact of U0 . n = (Opers (U0,B)) . n

proof

hence
( the charact of U0 = Opers (U0,B) & B is opers_closed )
by A2, A3, Th4, FINSEQ_1:13; :: thesis: verum
let n be Nat; :: thesis: ( n in dom the charact of U0 implies the charact of U0 . n = (Opers (U0,B)) . n )

assume A4: n in dom the charact of U0 ; :: thesis: the charact of U0 . n = (Opers (U0,B)) . n

then reconsider o = the charact of U0 . n as operation of U0 by FUNCT_1:def 3;

(Opers (U0,B)) . n = o /. B by A3, A4, Def6;

hence the charact of U0 . n = (Opers (U0,B)) . n by A2, Th4; :: thesis: verum

end;assume A4: n in dom the charact of U0 ; :: thesis: the charact of U0 . n = (Opers (U0,B)) . n

then reconsider o = the charact of U0 . n as operation of U0 by FUNCT_1:def 3;

(Opers (U0,B)) . n = o /. B by A3, A4, Def6;

hence the charact of U0 . n = (Opers (U0,B)) . n by A2, Th4; :: thesis: verum

hence ( the carrier of U1 is Subset of U0 & ( for B being non empty Subset of U0 st B = the carrier of U1 holds

( the charact of U1 = Opers (U0,B) & B is opers_closed ) ) ) by A1; :: thesis: verum