let N, M, K be ExtNat; :: thesis: K * (N + M) = (K * N) + (K * M)

per cases ( K is Nat or K = +infty ) by Th3;

suppose K is Nat ; :: thesis: K * (N + M) = (K * N) + (K * M)

hence K * (N + M) = (K * N) + (K * M) by XXREAL_3:95; :: thesis: verum

end;

suppose A1: K = +infty ; :: thesis: K * (N + M) = (K * N) + (K * M)

per cases ( ( N is positive & M is positive ) or not M is positive or not N is positive ) ;

suppose A2: ( N is positive & M is positive ) ; :: thesis: K * (N + M) = (K * N) + (K * M)

hence K * (N + M) = +infty by A1, XXREAL_3:def 5
.= (K * N) + +infty by XXREAL_3:def 2
.= (K * N) + (K * M) by A1, A2, XXREAL_3:def 5 ;
:: thesis: verum

end;

suppose not M is positive ; :: thesis: K * (N + M) = (K * N) + (K * M)

then A3: M = 0 ;
hence K * (N + M) = K * N by XXREAL_3:4
.= (K * N) + 0 by XXREAL_3:4
.= (K * N) + (K * M) by A3 ;
:: thesis: verum

end;

suppose not N is positive ; :: thesis: K * (N + M) = (K * N) + (K * M)

then A3: N = 0 ;
hence K * (N + M) = K * M by XXREAL_3:4
.= 0 + (K * M) by XXREAL_3:4
.= (K * N) + (K * M) by A3 ;
:: thesis: verum

end;

end;

end;

end;