let G be _finite _Graph; :: thesis: for S being VNumberingSeq of G

for m, n being Nat

for v being set st v in dom (S . m) & v in dom (S . n) holds

(S . m) . v = (S . n) . v

let S be VNumberingSeq of G; :: thesis: for m, n being Nat

for v being set st v in dom (S . m) & v in dom (S . n) holds

(S . m) . v = (S . n) . v

let m, n be Nat; :: thesis: for v being set st v in dom (S . m) & v in dom (S . n) holds

(S . m) . v = (S . n) . v

let v be set ; :: thesis: ( v in dom (S . m) & v in dom (S . n) implies (S . m) . v = (S . n) . v )

assume that

A1: v in dom (S . m) and

A2: v in dom (S . n) ; :: thesis: (S . m) . v = (S . n) . v

set VLM = S . m;

A3: [v,((S . m) . v)] in S . m by A1, FUNCT_1:def 2;

set VLN = S . n;

A4: [v,((S . n) . v)] in S . n by A2, FUNCT_1:def 2;

for m, n being Nat

for v being set st v in dom (S . m) & v in dom (S . n) holds

(S . m) . v = (S . n) . v

let S be VNumberingSeq of G; :: thesis: for m, n being Nat

for v being set st v in dom (S . m) & v in dom (S . n) holds

(S . m) . v = (S . n) . v

let m, n be Nat; :: thesis: for v being set st v in dom (S . m) & v in dom (S . n) holds

(S . m) . v = (S . n) . v

let v be set ; :: thesis: ( v in dom (S . m) & v in dom (S . n) implies (S . m) . v = (S . n) . v )

assume that

A1: v in dom (S . m) and

A2: v in dom (S . n) ; :: thesis: (S . m) . v = (S . n) . v

set VLM = S . m;

A3: [v,((S . m) . v)] in S . m by A1, FUNCT_1:def 2;

set VLN = S . n;

A4: [v,((S . n) . v)] in S . n by A2, FUNCT_1:def 2;