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 ) )
proof
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;
thus ( b = 1 implies drastic_norm . (a,b) = a ) :: thesis: ( a <> 1 & b <> 1 implies drastic_norm . (a,b) = 0 )
proof
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;
assume ( a <> 1 & b <> 1 ) ; :: thesis: drastic_norm . (a,b) = 0
then max (a,b) <> 1 by XXREAL_0:16;
hence drastic_norm . (a,b) = 0 by Drastic2Def; :: thesis: verum