let u be object ; :: thesis: ( u in(I % J)/\(I % K) implies u in I %(J + K) ) assume
u in(I % J)/\(I % K)
; :: thesis: u in I %(J + K) then A7:
ex x being Element of R st ( u = x & x in I % J & x in I % K )
; then consider a being Element of R such that A8:
u = a
and A9:
a * J c= I
; consider b being Element of R such that A10:
u = b
and A11:
b * K c= I
byA7;