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 ;
[y,x] in Flow M by ;
hence x in the carrier of M by ; :: 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 ;
A7: y in the carrier' of M by ;
[x,y] in Flow M by ;
hence x in the carrier of M by ; :: 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 ;
[y,x] in Flow M by ;
hence x in the carrier' of M by ; :: 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 ;
A13: y in the carrier of M by ;
[x,y] in Flow M by ;
hence x in the carrier' of M by ; :: 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 ; :: thesis: verum