set f = drastic_norm ;
FF: for a, b being Element of [.0,1.] holds drastic_norm . (a,b) = drastic_norm . (b,a)

proof

let a, b be Element of [.0,1.]; :: thesis:

per cases ;

suppose A1: a = 1 ; :: thesis:

then drastic_norm . (a,b) = b by DrasticDef;
hence drastic_norm . (a,b) = drastic_norm . (b,a) by A1, DrasticDef; :: thesis:

end;

suppose A1: b = 1 ; :: thesis:

then drastic_norm . (b,a) = a by DrasticDef;
hence drastic_norm . (a,b) = drastic_norm . (b,a) by A1, DrasticDef; :: thesis:

end;

suppose ( a <> 1 & b <> 1 ) ; :: thesis:

then ( drastic_norm . (a,b) = 0 & drastic_norm . (b,a) = 0 ) by DrasticDef;
hence drastic_norm . (a,b) = drastic_norm . (b,a) ; :: thesis:

end;

end;

end;

TT: for a being Element of [.0,1.] holds drastic_norm . (a,1) = a

proof

let a be Element of [.0,1.]; :: thesis:
1 in [.0,1.] by XXREAL_1:1;
hence drastic_norm . (a,1) = a by DrasticDef; :: thesis:

end;

D1: for a, b, c, d being Element of [.0,1.] st a <= c & b <= d holds
drastic_norm . (a,b) <= drastic_norm . (c,d)

proof

let a, b, c, d be Element of [.0,1.]; :: thesis:
B2: drastic_norm . (c,d) >= 0 by XXREAL_1:1;
assume S1: ( a <= c & b <= d ) ; :: thesis:

per cases ;

suppose S0: a = 1 ; :: thesis:

c <= 1 by XXREAL_1:1;
then drastic_norm . (c,d) = d by DrasticDef, S0, S1, XXREAL_0:1;
hence drastic_norm . (a,b) <= drastic_norm . (c,d) by S1, DrasticDef, S0; :: thesis:

end;

suppose S0: b = 1 ; :: thesis:

d <= 1 by XXREAL_1:1;
then drastic_norm . (c,d) = c by DrasticDef, S0, S1, XXREAL_0:1;
hence drastic_norm . (a,b) <= drastic_norm . (c,d) by S1, DrasticDef, S0; :: thesis:

end;

suppose ( b <> 1 & a <> 1 ) ; :: thesis:

hence drastic_norm . (a,b) <= drastic_norm . (c,d) by B2, DrasticDef; :: thesis:

end;

end;

end;

H1: 0 in [.0,1.] by XXREAL_1:1;
BU: for a being Element of [.0,1.] holds drastic_norm . (a,0) = 0

proof

let a be Element of [.0,1.]; :: thesis:
H2: 0 <= a by XXREAL_1:1;

per cases ;

suppose max (a,0) = 1 ; :: thesis:

then drastic_norm . (a,0) = min (a,0) by Drastic2Def, H1
.= 0 by H2, XXREAL_0:def 9 ;
hence drastic_norm . (a,0) = 0 ; :: thesis:

end;

suppose max (a,0) <> 1 ; :: thesis:

hence drastic_norm . (a,0) = 0 by Drastic2Def, H1; :: thesis:

end;

end;

end;

for a, b, c being Element of [.0,1.] holds drastic_norm . (a,(drastic_norm . (b,c))) = drastic_norm . ((drastic_norm . (a,b)),c)

proof

let a, b, c be Element of [.0,1.]; :: thesis:
Z4: min (a,b) in [.0,1.] by MinIn01;
EE: min (b,c) in [.0,1.] by MinIn01;

per cases ;

suppose Z1: ( max (a,b) = 1 & max (b,c) = 1 ) ; :: thesis:

then K1: ( a = 1 or b = 1 ) by XXREAL_0:16;
max (a,c) in [.0,1.] by MaxIn01;
then U2: max (a,c) <= 1 by XXREAL_1:1;
Z2: drastic_norm . (b,c) = min (b,c) by Drastic2Def, Z1;
UU: max (a,(min (b,c))) = min ((max (a,b)),(max (a,c))) by XXREAL_0:39
.= max (a,c) by U2, XXREAL_0:def 9, Z1 ;

per cases ;

suppose HU: max (a,c) = 1 ; :: thesis:

U2: max ((min (a,b)),c) = min ((max (a,c)),(max (b,c))) by XXREAL_0:39
.= 1 by Z1, HU ;
drastic_norm . (a,(drastic_norm . (b,c))) = drastic_norm . (a,(min (b,c))) by Drastic2Def, Z1
.= min (a,(min (b,c))) by Drastic2Def, HU, UU, EE
.= min ((min (a,b)),c) by XXREAL_0:33
.= drastic_norm . ((min (a,b)),c) by U2, Drastic2Def, Z4
.= drastic_norm . ((drastic_norm . (a,b)),c) by Drastic2Def, Z1 ;
hence drastic_norm . (a,(drastic_norm . (b,c))) = drastic_norm . ((drastic_norm . (a,b)),c) ; :: thesis:

end;

suppose HU: max (a,c) <> 1 ; :: thesis:

then a <= b by XXREAL_1:1, K1, DiffMax;
then K3: min (a,b) = a by XXREAL_0:def 9;
U1: drastic_norm . (a,b) = min (a,b) by Drastic2Def, Z1;
drastic_norm . (a,(drastic_norm . (b,c))) = 0 by Drastic2Def, HU, UU, Z2
.= drastic_norm . ((drastic_norm . (a,b)),c) by U1, K3, HU, Drastic2Def ;
hence drastic_norm . (a,(drastic_norm . (b,c))) = drastic_norm . ((drastic_norm . (a,b)),c) ; :: thesis:

end;

end;

end;

suppose Z1: ( max (a,b) = 1 & max (b,c) <> 1 ) ; :: thesis:

then z1: ( a = 1 or b = 1 ) by XXREAL_0:16;
max (b,c) in [.0,1.] by MaxIn01;
then W1: max (b,c) <= 1 by XXREAL_1:1;
za: b <> 1

proof

assume b = 1 ; :: thesis:
then max (b,c) >= 1 by XXREAL_0:25;
hence contradiction by Z1, XXREAL_0:1, W1; :: thesis:

end;

c <= 1 by XXREAL_1:1;
then z3: max (a,c) = 1 by z1, za, XXREAL_0:def 10;
qq: max ((min (a,b)),c) = min ((max (a,c)),(max (b,c))) by XXREAL_0:39
.= max (b,c) by W1, z3, XXREAL_0:def 9 ;
drastic_norm . (b,c) = 0 by Drastic2Def, Z1;
then drastic_norm . (a,(drastic_norm . (b,c))) = 0 by BU
.= drastic_norm . ((min (a,b)),c) by qq, Z1, Drastic2Def, Z4
.= drastic_norm . ((drastic_norm . (a,b)),c) by Drastic2Def, Z1 ;
hence drastic_norm . (a,(drastic_norm . (b,c))) = drastic_norm . ((drastic_norm . (a,b)),c) ; :: thesis:

end;

suppose Z1: ( max (a,b) <> 1 & max (b,c) = 1 ) ; :: thesis:

then z1: ( c = 1 or b = 1 ) by XXREAL_0:16;
max (a,b) in [.0,1.] by MaxIn01;
then w1: max (a,b) <= 1 by XXREAL_1:1;
zz: b <> 1

proof

assume b = 1 ; :: thesis:
then max (a,b) >= 1 by XXREAL_0:25;
hence contradiction by Z1, w1, XXREAL_0:1; :: thesis:

end;

Z2: drastic_norm . (b,c) = min (b,c) by Drastic2Def, Z1;
Y1: drastic_norm . (a,b) = 0 by Drastic2Def, Z1;
b <= c by XXREAL_1:1, zz, z1;
then drastic_norm . (b,c) = b by Z2, XXREAL_0:def 9;
then drastic_norm . (a,(drastic_norm . (b,c))) = 0 by Drastic2Def, Z1
.= drastic_norm . (c,0) by BU
.= drastic_norm . ((drastic_norm . (a,b)),c) by Y1, FF ;
hence drastic_norm . (a,(drastic_norm . (b,c))) = drastic_norm . ((drastic_norm . (a,b)),c) ; :: thesis:

end;

suppose Z1: ( max (a,b) <> 1 & max (b,c) <> 1 ) ; :: thesis:

then Z2: drastic_norm . (b,c) = 0 by Drastic2Def;
Z3: drastic_norm . (a,b) = 0 by Drastic2Def, Z1;
drastic_norm . (a,(drastic_norm . (b,c))) = 0 by BU, Z2
.= drastic_norm . (c,0) by BU
.= drastic_norm . ((drastic_norm . (a,b)),c) by Z3, FF ;
hence drastic_norm . (a,(drastic_norm . (b,c))) = drastic_norm . ((drastic_norm . (a,b)),c) ; :: thesis:

end;

end;

end;

hence ( drastic_norm is commutative & drastic_norm is associative & drastic_norm is with-1-identity & drastic_norm is monotonic ) by FF, TT, D1, BINOP_1:def 3, BINOP_1:def 2; :: thesis: