let a, b be Element of [.0,1.]; :: thesis: ( ( a = 1 implies drastic_norm . (a,b) = b ) & ( b = 1 implies drastic_norm . (a,b) = a ) & ( a <> 1 & b <> 1 implies drastic_norm . (a,b) = 0 ) )

A1: ( b <= 1 & a <= 1 ) by XXREAL_1:1;

thus ( a = 1 implies drastic_norm . (a,b) = b ) :: thesis: ( ( b = 1 implies drastic_norm . (a,b) = a ) & ( a <> 1 & b <> 1 implies drastic_norm . (a,b) = 0 ) )

then max (a,b) <> 1 by XXREAL_0:16;

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

A1: ( b <= 1 & a <= 1 ) by XXREAL_1:1;

thus ( a = 1 implies drastic_norm . (a,b) = b ) :: thesis: ( ( b = 1 implies drastic_norm . (a,b) = a ) & ( a <> 1 & b <> 1 implies drastic_norm . (a,b) = 0 ) )

proof

thus
( b = 1 implies drastic_norm . (a,b) = a )
:: thesis: ( a <> 1 & b <> 1 implies drastic_norm . (a,b) = 0 )
assume B1:
a = 1
; :: thesis: drastic_norm . (a,b) = b

then max (a,b) = 1 by A1, XXREAL_0:def 10;

then drastic_norm . (a,b) = min (a,b) by Drastic2Def

.= b by XXREAL_0:def 9, A1, B1 ;

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

end;then max (a,b) = 1 by A1, XXREAL_0:def 10;

then drastic_norm . (a,b) = min (a,b) by Drastic2Def

.= b by XXREAL_0:def 9, A1, B1 ;

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

proof

assume
( a <> 1 & b <> 1 )
; :: thesis: drastic_norm . (a,b) = 0
assume B1:
b = 1
; :: thesis: drastic_norm . (a,b) = a

then max (a,b) = 1 by A1, XXREAL_0:def 10;

then drastic_norm . (a,b) = min (a,b) by Drastic2Def

.= a by XXREAL_0:def 9, A1, B1 ;

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

end;then max (a,b) = 1 by A1, XXREAL_0:def 10;

then drastic_norm . (a,b) = min (a,b) by Drastic2Def

.= a by XXREAL_0:def 9, A1, B1 ;

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

then max (a,b) <> 1 by XXREAL_0:16;

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