let Z be set ; for I1, I2 being Function
for x being object st ((L_ x) \/ (R_ x)) \ {0_No} c= Z & I1 | Z = I2 | Z holds
( divL (x,I1) = divL (x,I2) & divR (x,I1) = divR (x,I2) )
let I1, I2 be Function; for x being object st ((L_ x) \/ (R_ x)) \ {0_No} c= Z & I1 | Z = I2 | Z holds
( divL (x,I1) = divL (x,I2) & divR (x,I1) = divR (x,I2) )
let x be object ; ( ((L_ x) \/ (R_ x)) \ {0_No} c= Z & I1 | Z = I2 | Z implies ( divL (x,I1) = divL (x,I2) & divR (x,I1) = divR (x,I2) ) )
assume A1:
( ((L_ x) \/ (R_ x)) \ {0_No} c= Z & I1 | Z = I2 | Z )
; ( divL (x,I1) = divL (x,I2) & divR (x,I1) = divR (x,I2) )
A2:
transitions_of (x,I1) = transitions_of (x,I2)
by A1, Th16;
A3:
( dom (divL (x,I1)) = NAT & NAT = dom (divL (x,I2)) )
by Def5;
for o being object st o in dom (divL (x,I1)) holds
(divL (x,I1)) . o = (divL (x,I2)) . o
proof
let o be
object ;
( o in dom (divL (x,I1)) implies (divL (x,I1)) . o = (divL (x,I2)) . o )
assume
o in dom (divL (x,I1))
;
(divL (x,I1)) . o = (divL (x,I2)) . o
then reconsider n =
o as
Nat by A3;
thus (divL (x,I1)) . o =
((transitions_of (x,I1)) . n) `1
by Def5
.=
(divL (x,I2)) . o
by A2, Def5
;
verum
end;
hence
divL (x,I1) = divL (x,I2)
by A3, FUNCT_1:2; divR (x,I1) = divR (x,I2)
A4:
( dom (divR (x,I1)) = NAT & NAT = dom (divR (x,I2)) )
by Def6;
for o being object st o in dom (divR (x,I1)) holds
(divR (x,I1)) . o = (divR (x,I2)) . o
proof
let o be
object ;
( o in dom (divR (x,I1)) implies (divR (x,I1)) . o = (divR (x,I2)) . o )
assume
o in dom (divR (x,I1))
;
(divR (x,I1)) . o = (divR (x,I2)) . o
then reconsider n =
o as
Nat by A4;
thus (divR (x,I1)) . o =
((transitions_of (x,I1)) . n) `2
by Def6
.=
(divR (x,I2)) . o
by Def6, A2
;
verum
end;
hence
divR (x,I1) = divR (x,I2)
by A4, FUNCT_1:2; verum