let I be set ; :: thesis: for k, x1, x2, y1, y2 being bag of I st x2 divides k & x1 divides (k -' x2) + y2 holds
( x2 + (x1 -' y2) divides k & (((k -' x2) + y2) -' x1) + y1 = (k -' (x2 + (x1 -' y2))) + ((y2 -' x1) + y1) )
let k, x1, x2, y1, y2 be bag of I; :: thesis: ( x2 divides k & x1 divides (k -' x2) + y2 implies ( x2 + (x1 -' y2) divides k & (((k -' x2) + y2) -' x1) + y1 = (k -' (x2 + (x1 -' y2))) + ((y2 -' x1) + y1) ) )
assume A1: for a being object holds x2 . a <= k . a ; :: according to PRE_POLY:def 11 :: thesis: ( not x1 divides (k -' x2) + y2 or ( x2 + (x1 -' y2) divides k & (((k -' x2) + y2) -' x1) + y1 = (k -' (x2 + (x1 -' y2))) + ((y2 -' x1) + y1) ) )
assume A2: for a being object holds x1 . a <= ((k -' x2) + y2) . a ; :: according to PRE_POLY:def 11 :: thesis: ( x2 + (x1 -' y2) divides k & (((k -' x2) + y2) -' x1) + y1 = (k -' (x2 + (x1 -' y2))) + ((y2 -' x1) + y1) )

hereby :: according to PRE_POLY:def 11 :: thesis: (((k -' x2) + y2) -' x1) + y1 = (k -' (x2 + (x1 -' y2))) + ((y2 -' x1) + y1)

let a be object ; :: thesis: (x2 + (x1 -' y2)) . a <= k . a
( x2 . a <= k . a & x1 . a <= ((k -' x2) + y2) . a & ((k -' x2) + y2) . a = ((k -' x2) . a) + (y2 . a) & ((k -' x2) . a) + (y2 . a) = ((k . a) -' (x2 . a)) + (y2 . a) ) by A1, A2, PRE_POLY:def 5, PRE_POLY:def 6;
then (x2 . a) + ((x1 . a) -' (y2 . a)) <= k . a by Th14;
then (x2 . a) + ((x1 -' y2) . a) <= k . a by PRE_POLY:def 6;
hence (x2 + (x1 -' y2)) . a <= k . a by PRE_POLY:def 5; :: thesis: verum

end;

let a be object ; :: according to PBOOLE:def 10 :: thesis: ( not a in I or ((((k -' x2) + y2) -' x1) + y1) . a = ((k -' (x2 + (x1 -' y2))) + ((y2 -' x1) + y1)) . a )
assume a in I ; :: thesis: ((((k -' x2) + y2) -' x1) + y1) . a = ((k -' (x2 + (x1 -' y2))) + ((y2 -' x1) + y1)) . a
( x2 . a <= k . a & x1 . a <= ((k -' x2) + y2) . a & ((k -' x2) + y2) . a = ((k -' x2) . a) + (y2 . a) & ((k -' x2) . a) + (y2 . a) = ((k . a) -' (x2 . a)) + (y2 . a) ) by A1, A2, PRE_POLY:def 5, PRE_POLY:def 6;
then A3: ((((k . a) -' (x2 . a)) + (y2 . a)) -' (x1 . a)) + (y1 . a) = ((k . a) -' ((x2 . a) + ((x1 . a) -' (y2 . a)))) + (((y2 . a) -' (x1 . a)) + (y1 . a)) by Th14;
A4: ((((k . a) -' (x2 . a)) + (y2 . a)) -' (x1 . a)) + (y1 . a) = ((((k -' x2) . a) + (y2 . a)) -' (x1 . a)) + (y1 . a) by PRE_POLY:def 6
.= ((((k -' x2) + y2) . a) -' (x1 . a)) + (y1 . a) by PRE_POLY:def 5
.= ((((k -' x2) + y2) -' x1) . a) + (y1 . a) by PRE_POLY:def 6
.= ((((k -' x2) + y2) -' x1) + y1) . a by PRE_POLY:def 5 ;
((k . a) -' ((x2 . a) + ((x1 . a) -' (y2 . a)))) + (((y2 . a) -' (x1 . a)) + (y1 . a)) = ((k . a) -' ((x2 . a) + ((x1 . a) -' (y2 . a)))) + (((y2 -' x1) . a) + (y1 . a)) by PRE_POLY:def 6
.= ((k . a) -' ((x2 . a) + ((x1 -' y2) . a))) + (((y2 -' x1) . a) + (y1 . a)) by PRE_POLY:def 6
.= ((k . a) -' ((x2 + (x1 -' y2)) . a)) + (((y2 -' x1) . a) + (y1 . a)) by PRE_POLY:def 5
.= ((k . a) -' ((x2 + (x1 -' y2)) . a)) + (((y2 -' x1) + y1) . a) by PRE_POLY:def 5
.= ((k -' (x2 + (x1 -' y2))) . a) + (((y2 -' x1) + y1) . a) by PRE_POLY:def 6 ;
hence ((((k -' x2) + y2) -' x1) + y1) . a = ((k -' (x2 + (x1 -' y2))) + ((y2 -' x1) + y1)) . a by A3, A4, PRE_POLY:def 5; :: thesis: verum