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