let x be Element of carr f; :: thesis: ( ( a in [#] K & b in [#] K & ( a = 0. K or b = 0. K ) implies ( x = the multF of K . (a,b) iff x = 0. K ) ) & ( a in [#] K & b in [#] K & a in [#] K & a <> 0. K & not b in [#] K implies ( x = the multF of K . (a,b) iff x = the multF of T . ((f . a),b) ) ) & ( a in [#] K & b in [#] K & b in [#] K & b <> 0. K & not a in [#] K implies ( x = the multF of K . (a,b) iff x = the multF of T . (a,(f . b)) ) ) & ( a in [#] K & b in [#] K & not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f implies ( x = the multF of K . (a,b) iff x = (f ") . ( the multF of T . (a,b)) ) ) & ( ( a = 0. K or b = 0. K ) & a in [#] K & a <> 0. K & not b in [#] K implies ( x = 0. K iff x = the multF of T . ((f . a),b) ) ) & ( ( a = 0. K or b = 0. K ) & b in [#] K & b <> 0. K & not a in [#] K implies ( x = 0. K iff x = the multF of T . (a,(f . b)) ) ) & ( ( a = 0. K or b = 0. K ) & not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f implies ( x = 0. K iff x = (f ") . ( the multF of T . (a,b)) ) ) & ( a in [#] K & a <> 0. K & not b in [#] K & b in [#] K & b <> 0. K & not a in [#] K implies ( x = the multF of T . ((f . a),b) iff x = the multF of T . (a,(f . b)) ) ) & ( a in [#] K & a <> 0. K & not b in [#] K & not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f implies ( x = the multF of T . ((f . a),b) iff x = (f ") . ( the multF of T . (a,b)) ) ) & ( b in [#] K & b <> 0. K & not a in [#] K & not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f implies ( x = the multF of T . (a,(f . b)) iff x = (f ") . ( the multF of T . (a,b)) ) ) )

now :: thesis: ( a in [#] K & b in [#] K & ( a = 0. K or b = 0. K ) implies ( x = the multF of K . (a,b) iff x = 0. K ) )

assume A1: ( a in [#] K & b in [#] K & ( a = 0. K or b = 0. K ) ) ; :: thesis: ( x = the multF of K . (a,b) iff x = 0. K )
then reconsider a1 = a, b1 = b as Element of K ;

per cases ( a = 0. K or b = 0. K ) by A1;

suppose a = 0. K ; :: thesis: ( x = the multF of K . (a,b) iff x = 0. K )

then 0. K = a1 * b1
.= the multF of K . (a,b) ;
hence ( x = the multF of K . (a,b) iff x = 0. K ) ; :: thesis: verum

end;

suppose b = 0. K ; :: thesis: ( x = the multF of K . (a,b) iff x = 0. K )

then 0. K = a1 * b1
.= the multF of K . (a,b) ;
hence ( x = the multF of K . (a,b) iff x = 0. K ) ; :: thesis: verum

end;

end;

end;

hence ( ( a in [#] K & b in [#] K & ( a = 0. K or b = 0. K ) implies ( x = the multF of K . (a,b) iff x = 0. K ) ) & ( a in [#] K & b in [#] K & a in [#] K & a <> 0. K & not b in [#] K implies ( x = the multF of K . (a,b) iff x = the multF of T . ((f . a),b) ) ) & ( a in [#] K & b in [#] K & b in [#] K & b <> 0. K & not a in [#] K implies ( x = the multF of K . (a,b) iff x = the multF of T . (a,(f . b)) ) ) & ( a in [#] K & b in [#] K & not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f implies ( x = the multF of K . (a,b) iff x = (f ") . ( the multF of T . (a,b)) ) ) & ( ( a = 0. K or b = 0. K ) & a in [#] K & a <> 0. K & not b in [#] K implies ( x = 0. K iff x = the multF of T . ((f . a),b) ) ) & ( ( a = 0. K or b = 0. K ) & b in [#] K & b <> 0. K & not a in [#] K implies ( x = 0. K iff x = the multF of T . (a,(f . b)) ) ) & ( ( a = 0. K or b = 0. K ) & not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f implies ( x = 0. K iff x = (f ") . ( the multF of T . (a,b)) ) ) & ( a in [#] K & a <> 0. K & not b in [#] K & b in [#] K & b <> 0. K & not a in [#] K implies ( x = the multF of T . ((f . a),b) iff x = the multF of T . (a,(f . b)) ) ) & ( a in [#] K & a <> 0. K & not b in [#] K & not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f implies ( x = the multF of T . ((f . a),b) iff x = (f ") . ( the multF of T . (a,b)) ) ) & ( b in [#] K & b <> 0. K & not a in [#] K & not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f implies ( x = the multF of T . (a,(f . b)) iff x = (f ") . ( the multF of T . (a,b)) ) ) ) ; :: thesis: verum