let a, b be object ; :: thesis: for X, Z being set
for I1, I2 being Function st X \ {0_No} c= Z & I1 | Z = I2 | Z holds
divs (a,b,X,I1) = divs (a,b,X,I2)
let X, Z be set ; :: thesis: for I1, I2 being Function st X \ {0_No} c= Z & I1 | Z = I2 | Z holds
divs (a,b,X,I1) = divs (a,b,X,I2)
let I1, I2 be Function; :: thesis: ( X \ {0_No} c= Z & I1 | Z = I2 | Z implies divs (a,b,X,I1) = divs (a,b,X,I2) )
assume A1: ( X \ {0_No} c= Z & I1 | Z = I2 | Z ) ; :: thesis: divs (a,b,X,I1) = divs (a,b,X,I2)
thus divs (a,b,X,I1) c= divs (a,b,X,I2) :: according to XBOOLE_0:def 10 :: thesis: divs (a,b,X,I2) c= divs (a,b,X,I1)

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in divs (a,b,X,I1) or o in divs (a,b,X,I2) )
assume o in divs (a,b,X,I1) ; :: thesis: o in divs (a,b,X,I2)
then consider xL being object such that
A2: ( xL in X & xL <> 0_No & o = (1_No +' ((xL +' (-' b)) *' a)) *' (I1 . xL) ) by Def2;
A3: xL in X \ {0_No} by A2, ZFMISC_1:56;
then I1 . xL = (I2 | Z) . xL by A1, FUNCT_1:49
.= I2 . xL by A3, A1, FUNCT_1:49 ;
hence o in divs (a,b,X,I2) by A2, Def2; :: thesis: verum

end;

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in divs (a,b,X,I2) or o in divs (a,b,X,I1) )
assume o in divs (a,b,X,I2) ; :: thesis: o in divs (a,b,X,I1)
then consider xL being object such that
A4: ( xL in X & xL <> 0_No & o = (1_No +' ((xL +' (-' b)) *' a)) *' (I2 . xL) ) by Def2;
A5: xL in X \ {0_No} by A4, ZFMISC_1:56;
then I2 . xL = (I1 | Z) . xL by A1, FUNCT_1:49
.= I1 . xL by A5, A1, FUNCT_1:49 ;
hence o in divs (a,b,X,I1) by A4, Def2; :: thesis: verum