reconsider f = id (bool A) as Function of (bool A),(bool A) ;

{} c= A ;

then A1: f . {} = {} by FUNCT_1:18;

A in bool A by ZFMISC_1:def 1;

then f . A = A by FUNCT_1:18;

hence for b_{1} being Function of (bool A),(bool A) st b_{1} = id (bool A) holds

( b_{1} is empty-preserving & b_{1} is universe-preserving )
by A1; :: thesis: verum

{} c= A ;

then A1: f . {} = {} by FUNCT_1:18;

A in bool A by ZFMISC_1:def 1;

then f . A = A by FUNCT_1:18;

hence for b

( b