let f, g be Function; :: thesis: ( dom f misses dom g & rng g misses dom f implies for X being set holds f * (X -indexing g) = f | X )
assume that
A1: dom f misses dom g and
A2: rng g misses dom f ; :: thesis: for X being set holds f * (X -indexing g) = f | X
let X be set ; :: thesis: f * (X -indexing g) = f | X
A3: dom (f | X) c= dom f by RELAT_1:60;
A4: (id X) .: (dom (g | X)) c= dom (g | X)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (id X) .: (dom (g | X)) or x in dom (g | X) )
assume x in (id X) .: (dom (g | X)) ; :: thesis: x in dom (g | X)
then ex y being object st
( y in dom (id X) & y in dom (g | X) & x = (id X) . y ) by FUNCT_1:def 6;
hence x in dom (g | X) by FUNCT_1:18; :: thesis: verum
end;
dom (g | X) c= dom g by RELAT_1:60;
then dom (f | X) misses dom (g | X) by A1, A3, XBOOLE_1:64;
then A5: (id X) .: (dom (g | X)) misses dom (f | X) by A4, XBOOLE_1:64;
A6: dom (f | X) c= X by RELAT_1:58;
rng (g | X) c= rng g by RELAT_1:70;
then A7: dom (f | X) misses rng (g | X) by A2, A3, XBOOLE_1:64;
g .: X c= rng g by RELAT_1:111;
then g .: X misses dom f by A2, XBOOLE_1:64;
then A8: (g .: X) /\ (dom f) = {} ;
rng (X -indexing g) = (X \ (dom g)) \/ (g .: X) by Th7;
then (rng (X -indexing g)) /\ (dom f) = ((X \ (dom g)) /\ (dom f)) \/ ((g .: X) /\ (dom f)) by XBOOLE_1:23
.= (X \ (dom g)) /\ (dom f) by A8 ;
then (rng (X -indexing g)) /\ (dom f) c= X /\ (dom f) by XBOOLE_1:26;
then (rng (X -indexing g)) /\ (dom f) c= dom (f | X) by RELAT_1:61;
hence f * (X -indexing g) = (f | X) * ((id X) +* (g | X)) by Th2, RELAT_1:59
.= (f | X) * (id X) by A7, A5, Th3
.= f | X by A6, RELAT_1:51 ;
:: thesis: verum