let Z be set ; :: thesis: for I1, I2 being Function
for x being object st ((L_ x) \/ (R_ x)) \ {0_No} c= Z & I1 | Z = I2 | Z holds
transitions_of (x,I1) = transitions_of (x,I2)
let I1, I2 be Function; :: thesis: for x being object st ((L_ x) \/ (R_ x)) \ {0_No} c= Z & I1 | Z = I2 | Z holds
transitions_of (x,I1) = transitions_of (x,I2)
let x be object ; :: thesis: ( ((L_ x) \/ (R_ x)) \ {0_No} c= Z & I1 | Z = I2 | Z implies transitions_of (x,I1) = transitions_of (x,I2) )
assume A1: ( ((L_ x) \/ (R_ x)) \ {0_No} c= Z & I1 | Z = I2 | Z ) ; :: thesis: transitions_of (x,I1) = transitions_of (x,I2)
set T1 = transitions_of (x,I1);
set T2 = transitions_of (x,I2);
defpred S₁[ Nat] means (transitions_of (x,I1)) . $1 = (transitions_of (x,I2)) . $1;
(transitions_of (x,I1)) . 0 = 1_No by Def4;
then A2: S₁[ 0 ] by Def4;
A3: ( (L_ x) \ {0_No} c= ((L_ x) \/ (R_ x)) \ {0_No} & (R_ x) \ {0_No} c= ((L_ x) \/ (R_ x)) \ {0_No} ) by XBOOLE_1:7, XBOOLE_1:33;
A4: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A5: S₁[n] ; :: thesis: S₁[n + 1]
A6: ( (transitions_of (x,I1)) . (n + 1) is pair & (transitions_of (x,I2)) . (n + 1) is pair ) by Def4;
A7: ((transitions_of (x,I1)) . (n + 1)) `1 = ((L_ ((transitions_of (x,I1)) . n)) \/ (divset ((L_ ((transitions_of (x,I1)) . n)),x,(R_ x),I1))) \/ (divset ((R_ ((transitions_of (x,I1)) . n)),x,(L_ x),I1)) by Def4
.= ((L_ ((transitions_of (x,I1)) . n)) \/ (divset ((L_ ((transitions_of (x,I1)) . n)),x,(R_ x),I2))) \/ (divset ((R_ ((transitions_of (x,I1)) . n)),x,(L_ x),I1)) by A1, A3, XBOOLE_1:1, Th15
.= ((L_ ((transitions_of (x,I2)) . n)) \/ (divset ((L_ ((transitions_of (x,I2)) . n)),x,(R_ x),I2))) \/ (divset ((R_ ((transitions_of (x,I2)) . n)),x,(L_ x),I2)) by A1, A3, XBOOLE_1:1, Th15, A5
.= ((transitions_of (x,I2)) . (n + 1)) `1 by Def4 ;
((transitions_of (x,I1)) . (n + 1)) `2 = ((R_ ((transitions_of (x,I1)) . n)) \/ (divset ((L_ ((transitions_of (x,I1)) . n)),x,(L_ x),I1))) \/ (divset ((R_ ((transitions_of (x,I1)) . n)),x,(R_ x),I1)) by Def4
.= ((R_ ((transitions_of (x,I1)) . n)) \/ (divset ((L_ ((transitions_of (x,I1)) . n)),x,(L_ x),I1))) \/ (divset ((R_ ((transitions_of (x,I1)) . n)),x,(R_ x),I2)) by A1, A3, XBOOLE_1:1, Th15
.= ((R_ ((transitions_of (x,I2)) . n)) \/ (divset ((L_ ((transitions_of (x,I2)) . n)),x,(L_ x),I2))) \/ (divset ((R_ ((transitions_of (x,I2)) . n)),x,(R_ x),I2)) by A1, A3, XBOOLE_1:1, Th15, A5
.= ((transitions_of (x,I2)) . (n + 1)) `2 by Def4 ;
hence S₁[n + 1] by A6, A7, XTUPLE_0:2; :: thesis: verum

end;

A8: for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A4);
A9: ( dom (transitions_of (x,I1)) = NAT & NAT = dom (transitions_of (x,I2)) ) by Def4;
then for o being object st o in dom (transitions_of (x,I1)) holds
(transitions_of (x,I1)) . o = (transitions_of (x,I2)) . o by A8;
hence transitions_of (x,I1) = transitions_of (x,I2) by A9, FUNCT_1:2; :: thesis: verum