set f = drastic_norm ;

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

drastic_norm . (a,b) <= drastic_norm . (c,d)

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

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

proof

TT:
for a being Element of [.0,1.] holds drastic_norm . (a,1) = a
let a, b be Element of [.0,1.]; :: thesis: drastic_norm . (a,b) = drastic_norm . (b,a)

end;per cases
( a = 1 or b = 1 or ( a <> 1 & b <> 1 ) )
;

end;

suppose A1:
a = 1
; :: thesis: drastic_norm . (a,b) = drastic_norm . (b,a)

then
drastic_norm . (a,b) = b
by DrasticDef;

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

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

suppose A1:
b = 1
; :: thesis: drastic_norm . (a,b) = drastic_norm . (b,a)

then
drastic_norm . (b,a) = a
by DrasticDef;

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

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

suppose
( a <> 1 & b <> 1 )
; :: thesis: drastic_norm . (a,b) = drastic_norm . (b,a)

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

hence drastic_norm . (a,b) = drastic_norm . (b,a) ; :: thesis: verum

end;hence drastic_norm . (a,b) = drastic_norm . (b,a) ; :: thesis: verum

proof

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

1 in [.0,1.] by XXREAL_1:1;

hence drastic_norm . (a,1) = a by DrasticDef; :: thesis: verum

end;1 in [.0,1.] by XXREAL_1:1;

hence drastic_norm . (a,1) = a by DrasticDef; :: thesis: verum

drastic_norm . (a,b) <= drastic_norm . (c,d)

proof

H1:
0 in [.0,1.]
by XXREAL_1:1;
let a, b, c, d be Element of [.0,1.]; :: thesis: ( a <= c & b <= d implies drastic_norm . (a,b) <= drastic_norm . (c,d) )

B2: drastic_norm . (c,d) >= 0 by XXREAL_1:1;

assume S1: ( a <= c & b <= d ) ; :: thesis: drastic_norm . (a,b) <= drastic_norm . (c,d)

end;B2: drastic_norm . (c,d) >= 0 by XXREAL_1:1;

assume S1: ( a <= c & b <= d ) ; :: thesis: drastic_norm . (a,b) <= drastic_norm . (c,d)

per cases
( a = 1 or b = 1 or ( b <> 1 & a <> 1 ) )
;

end;

suppose S0:
a = 1
; :: thesis: drastic_norm . (a,b) <= drastic_norm . (c,d)

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: verum

end;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: verum

suppose S0:
b = 1
; :: thesis: drastic_norm . (a,b) <= drastic_norm . (c,d)

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: verum

end;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: verum

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

proof

for a, b, c being Element of [.0,1.] holds drastic_norm . (a,(drastic_norm . (b,c))) = drastic_norm . ((drastic_norm . (a,b)),c)
let a be Element of [.0,1.]; :: thesis: drastic_norm . (a,0) = 0

H2: 0 <= a by XXREAL_1:1;

end;H2: 0 <= a by XXREAL_1:1;

per cases
( max (a,0) = 1 or max (a,0) <> 1 )
;

end;

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

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: verum

end;.= 0 by H2, XXREAL_0:def 9 ;

hence drastic_norm . (a,0) = 0 ; :: thesis: verum

proof

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: verum
let a, b, c be Element of [.0,1.]; :: thesis: drastic_norm . (a,(drastic_norm . (b,c))) = drastic_norm . ((drastic_norm . (a,b)),c)

Z4: min (a,b) in [.0,1.] by MinIn01;

EE: min (b,c) in [.0,1.] by MinIn01;

end;Z4: min (a,b) in [.0,1.] by MinIn01;

EE: min (b,c) in [.0,1.] by MinIn01;

per cases
( ( max (a,b) = 1 & max (b,c) = 1 ) or ( max (a,b) = 1 & max (b,c) <> 1 ) or ( max (a,b) <> 1 & max (b,c) = 1 ) or ( max (a,b) <> 1 & max (b,c) <> 1 ) )
;

end;

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

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 ;

end;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
( max (a,c) = 1 or max (a,c) <> 1 )
;

end;

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

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: verum

end;.= 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: verum

suppose HU:
max (a,c) <> 1
; :: thesis: drastic_norm . (a,(drastic_norm . (b,c))) = drastic_norm . ((drastic_norm . (a,b)),c)

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: verum

end;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: verum

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

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

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: verum

end;max (b,c) in [.0,1.] by MaxIn01;

then W1: max (b,c) <= 1 by XXREAL_1:1;

za: b <> 1

proof

c <= 1
by XXREAL_1:1;
assume
b = 1
; :: thesis: contradiction

then max (b,c) >= 1 by XXREAL_0:25;

hence contradiction by Z1, XXREAL_0:1, W1; :: thesis: verum

end;then max (b,c) >= 1 by XXREAL_0:25;

hence contradiction by Z1, XXREAL_0:1, W1; :: thesis: verum

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: verum

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

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

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: verum

end;max (a,b) in [.0,1.] by MaxIn01;

then w1: max (a,b) <= 1 by XXREAL_1:1;

zz: b <> 1

proof

Z2:
drastic_norm . (b,c) = min (b,c)
by Drastic2Def, Z1;
assume
b = 1
; :: thesis: contradiction

then max (a,b) >= 1 by XXREAL_0:25;

hence contradiction by Z1, w1, XXREAL_0:1; :: thesis: verum

end;then max (a,b) >= 1 by XXREAL_0:25;

hence contradiction by Z1, w1, XXREAL_0:1; :: thesis: verum

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: verum

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

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: verum

end;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: verum