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
proof
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;
A4: for x being object st x in rng (((Flow M) ~) | the carrier' of M) holds
x in the carrier of M
proof
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;
A8: for x being object st x in rng ((Flow M) | the carrier of M) holds
x in the carrier' of M
proof
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;
for x being object st x in rng (((Flow M) ~) | the carrier of M) holds
x in the carrier' of M
proof
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;
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