let D1, D2 be Function; :: thesis: ( dom D1 = NAT & ( for k being Nat holds D1 . k = ((transitions_of (x0,x)) . k) `2 ) & dom D2 = NAT & ( for k being Nat holds D2 . k = ((transitions_of (x0,x)) . k) `2 ) implies D1 = D2 )
assume that
A3: ( dom D1 = NAT & ( for k being Nat holds D1 . k = ((transitions_of (x0,x)) . k) `2 ) ) and
A4: ( dom D2 = NAT & ( for k being Nat holds D2 . k = ((transitions_of (x0,x)) . k) `2 ) ) ; :: thesis: D1 = D2
for o being object st o in dom D1 holds
D1 . o = D2 . o

proof

let o be object ; :: thesis: ( o in dom D1 implies D1 . o = D2 . o )
assume o in dom D1 ; :: thesis: D1 . o = D2 . o
then reconsider a = o as Nat by A3;
thus D1 . o = ((transitions_of (x0,x)) . a) `2 by A3
.= D2 . o by A4 ; :: thesis: verum

end;

hence D1 = D2 by A3, A4, FUNCT_1:2; :: thesis: verum