let M be Pnet; :: thesis: ( rng ((Flow M) | the carrier' of M) c= the carrier of M & rng (((Flow M) ~) | the carrier' of M) c= the carrier of M & rng ((Flow M) | the carrier of M) c= the carrier' of M & rng (((Flow M) ~) | the carrier of M) c= the carrier' of M & rng (id the carrier' of M) c= the carrier' of M & dom (id the carrier' of M) c= the carrier' of M & rng (id the carrier of M) c= the carrier of M & dom (id the carrier of M) c= the carrier of M )

A1: for x being object st x in rng ((Flow M) | the carrier' of M) holds

x in the carrier of M

x in the carrier of M

x in the carrier' of M

x in the carrier' of M

A1: for x being object st x in rng ((Flow M) | the carrier' of M) holds

x in the carrier of M

proof

A4:
for x being object st x in rng (((Flow M) ~) | the carrier' of M) holds
let x be object ; :: thesis: ( x in rng ((Flow M) | the carrier' of M) implies x in the carrier of M )

assume x in rng ((Flow M) | the carrier' of M) ; :: thesis: x in the carrier of M

then consider y being object such that

A2: [y,x] in (Flow M) | the carrier' of M by XTUPLE_0:def 13;

A3: y in the carrier' of M by A2, RELAT_1:def 11;

[y,x] in Flow M by A2, RELAT_1:def 11;

hence x in the carrier of M by A3, Th7; :: thesis: verum

end;assume x in rng ((Flow M) | the carrier' of M) ; :: thesis: x in the carrier of M

then consider y being object such that

A2: [y,x] in (Flow M) | the carrier' of M by XTUPLE_0:def 13;

A3: y in the carrier' of M by A2, RELAT_1:def 11;

[y,x] in Flow M by A2, RELAT_1:def 11;

hence x in the carrier of M by A3, Th7; :: thesis: verum

x in the carrier of M

proof

A8:
for x being object st x in rng ((Flow M) | the carrier of M) holds
let x be object ; :: thesis: ( x in rng (((Flow M) ~) | the carrier' of M) implies x in the carrier of M )

assume x in rng (((Flow M) ~) | the carrier' of M) ; :: thesis: x in the carrier of M

then consider y being object such that

A5: [y,x] in ((Flow M) ~) | the carrier' of M by XTUPLE_0:def 13;

A6: [y,x] in (Flow M) ~ by A5, RELAT_1:def 11;

A7: y in the carrier' of M by A5, RELAT_1:def 11;

[x,y] in Flow M by A6, RELAT_1:def 7;

hence x in the carrier of M by A7, Th7; :: thesis: verum

end;assume x in rng (((Flow M) ~) | the carrier' of M) ; :: thesis: x in the carrier of M

then consider y being object such that

A5: [y,x] in ((Flow M) ~) | the carrier' of M by XTUPLE_0:def 13;

A6: [y,x] in (Flow M) ~ by A5, RELAT_1:def 11;

A7: y in the carrier' of M by A5, RELAT_1:def 11;

[x,y] in Flow M by A6, RELAT_1:def 7;

hence x in the carrier of M by A7, Th7; :: thesis: verum

x in the carrier' of M

proof

for x being object st x in rng (((Flow M) ~) | the carrier of M) holds
let x be object ; :: thesis: ( x in rng ((Flow M) | the carrier of M) implies x in the carrier' of M )

assume x in rng ((Flow M) | the carrier of M) ; :: thesis: x in the carrier' of M

then consider y being object such that

A9: [y,x] in (Flow M) | the carrier of M by XTUPLE_0:def 13;

A10: y in the carrier of M by A9, RELAT_1:def 11;

[y,x] in Flow M by A9, RELAT_1:def 11;

hence x in the carrier' of M by A10, Th7; :: thesis: verum

end;assume x in rng ((Flow M) | the carrier of M) ; :: thesis: x in the carrier' of M

then consider y being object such that

A9: [y,x] in (Flow M) | the carrier of M by XTUPLE_0:def 13;

A10: y in the carrier of M by A9, RELAT_1:def 11;

[y,x] in Flow M by A9, RELAT_1:def 11;

hence x in the carrier' of M by A10, Th7; :: thesis: verum

x in the carrier' of M

proof

hence
( rng ((Flow M) | the carrier' of M) c= the carrier of M & rng (((Flow M) ~) | the carrier' of M) c= the carrier of M & rng ((Flow M) | the carrier of M) c= the carrier' of M & rng (((Flow M) ~) | the carrier of M) c= the carrier' of M & rng (id the carrier' of M) c= the carrier' of M & dom (id the carrier' of M) c= the carrier' of M & rng (id the carrier of M) c= the carrier of M & dom (id the carrier of M) c= the carrier of M )
by A1, A4, A8, TARSKI:def 3; :: thesis: verum
let x be object ; :: thesis: ( x in rng (((Flow M) ~) | the carrier of M) implies x in the carrier' of M )

assume x in rng (((Flow M) ~) | the carrier of M) ; :: thesis: x in the carrier' of M

then consider y being object such that

A11: [y,x] in ((Flow M) ~) | the carrier of M by XTUPLE_0:def 13;

A12: [y,x] in (Flow M) ~ by A11, RELAT_1:def 11;

A13: y in the carrier of M by A11, RELAT_1:def 11;

[x,y] in Flow M by A12, RELAT_1:def 7;

hence x in the carrier' of M by A13, Th7; :: thesis: verum

end;assume x in rng (((Flow M) ~) | the carrier of M) ; :: thesis: x in the carrier' of M

then consider y being object such that

A11: [y,x] in ((Flow M) ~) | the carrier of M by XTUPLE_0:def 13;

A12: [y,x] in (Flow M) ~ by A11, RELAT_1:def 11;

A13: y in the carrier of M by A11, RELAT_1:def 11;

[x,y] in Flow M by A12, RELAT_1:def 7;

hence x in the carrier' of M by A13, Th7; :: thesis: verum