let I be non degenerated commutative domRing-like Ring; :: thesis: for u, v, w being Element of Quot. I holds (quotmult I) . (u,((quotadd I) . (v,w))) = (quotadd I) . (((quotmult I) . (u,v)),((quotmult I) . (u,w)))
let u, v, w be Element of Quot. I; :: thesis: (quotmult I) . (u,((quotadd I) . (v,w))) = (quotadd I) . (((quotmult I) . (u,v)),((quotmult I) . (u,w)))
(quotmult I) . (u,((quotadd I) . (v,w))) = (quotmult I) . (u,(qadd (v,w))) by Def12
.= qmult (u,(qadd (v,w))) by Def13
.= qadd ((qmult (u,v)),(qmult (u,w))) by Th16
.= qadd (((quotmult I) . (u,v)),(qmult (u,w))) by Def13
.= qadd (((quotmult I) . (u,v)),((quotmult I) . (u,w))) by Def13
.= (quotadd I) . (((quotmult I) . (u,v)),((quotmult I) . (u,w))) by Def12 ;
hence (quotmult I) . (u,((quotadd I) . (v,w))) = (quotadd I) . (((quotmult I) . (u,v)),((quotmult I) . (u,w))) ; :: thesis: verum