let V be set ; :: thesis: for G being Graph
for pe being FinSequence of the carrier' of G holds
( vertices pe c= V iff for i being Nat st i in dom pe holds
vertices (pe /. i) c= V )
let G be Graph; :: thesis: for pe being FinSequence of the carrier' of G holds
( vertices pe c= V iff for i being Nat st i in dom pe holds
vertices (pe /. i) c= V )
let pe be FinSequence of the carrier' of G; :: thesis: ( vertices pe c= V iff for i being Nat st i in dom pe holds
vertices (pe /. i) c= V )
set FS = the Source of G;
set FT = the Target of G;
hereby :: thesis: ( ( for i being Nat st i in dom pe holds
vertices (pe /. i) c= V ) implies vertices pe c= V )
assume A1: vertices pe c= V ; :: thesis: for i being Nat st i in dom pe holds
vertices (pe /. i) c= V
hereby :: thesis: verum
let i be Nat; :: thesis: ( i in dom pe implies vertices (pe /. i) c= V )
assume A2: i in dom pe ; :: thesis: vertices (pe /. i) c= V
then A3: ( 1 <= i & i <= len pe ) by FINSEQ_3:25;
thus vertices (pe /. i) c= V :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in vertices (pe /. i) or x in V )
assume A4: x in vertices (pe /. i) ; :: thesis: x in V
then ( x = the Source of G . (pe /. i) or x = the Target of G . (pe /. i) ) by TARSKI:def 2;
then ( x = the Source of G . (pe . i) or x = the Target of G . (pe . i) ) by A3, FINSEQ_4:15;
then reconsider y = x as Vertex of G by A2, FINSEQ_2:11, FUNCT_2:5;
y in { v where v is Vertex of G : ex i being Nat st
( i in dom pe & v in vertices (pe /. i) ) } by A2, A4;
hence x in V by A1; :: thesis: verum
end;
end;
end;
assume A5: for i being Nat st i in dom pe holds
vertices (pe /. i) c= V ; :: thesis: vertices pe c= V
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in vertices pe or x in V )
assume x in vertices pe ; :: thesis: x in V
then consider y being Vertex of G such that
A6: y = x and
A7: ex i being Nat st
( i in dom pe & y in vertices (pe /. i) ) ;
consider i being Nat such that
A8: i in dom pe and
A9: y in vertices (pe /. i) by A7;
vertices (pe /. i) c= V by A5, A8;
hence x in V by A6, A9; :: thesis: verum