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;

per cases ( m <= n or m > n ) ;

suppose m <= n ; :: thesis: (S . m) . v = (S . n) . v

then S . m c= S . n by Th17;
hence (S . m) . v = (S . n) . v by A2, A3, FUNCT_1:def 2; :: thesis: verum

end;

suppose m > n ; :: thesis: (S . m) . v = (S . n) . v

then S . n c= S . m by Th17;
hence (S . m) . v = (S . n) . v by A1, A4, FUNCT_1:def 2; :: thesis: verum

end;

end;