let f, g be one-to-one Function; :: thesis: ( dom f misses dom g & rng f misses rng g implies (f +* g) " = (f ") +* (g ") )
assume that
A1: dom f misses dom g and
A2: rng f misses rng g ; :: thesis: (f +* g) " = (f ") +* (g ")
A3: f +* g is one-to-one by ;
A4: for y, x being object holds
( y in rng (f +* g) & x = ((f ") +* (g ")) . y iff ( x in dom (f +* g) & y = (f +* g) . x ) )
proof
let y, x be object ; :: thesis: ( y in rng (f +* g) & x = ((f ") +* (g ")) . y iff ( x in dom (f +* g) & y = (f +* g) . x ) )
thus ( y in rng (f +* g) & x = ((f ") +* (g ")) . y implies ( x in dom (f +* g) & y = (f +* g) . x ) ) :: thesis: ( x in dom (f +* g) & y = (f +* g) . x implies ( y in rng (f +* g) & x = ((f ") +* (g ")) . y ) )
proof
A5: rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;
assume that
A6: y in rng (f +* g) and
A7: x = ((f ") +* (g ")) . y ; :: thesis: ( x in dom (f +* g) & y = (f +* g) . x )
per cases ( y in rng f or y in rng g ) by ;
suppose A8: y in rng f ; :: thesis: ( x in dom (f +* g) & y = (f +* g) . x )
then consider z being object such that
A9: z in dom f and
A10: y = f . z by FUNCT_1:def 3;
dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def 1;
then A11: z in dom (f +* g) by ;
A12: ( dom (f ") = rng f & dom (g ") = rng g ) by FUNCT_1:33;
( y = (f +* g) . z & z = (f ") . y ) by ;
hence ( x in dom (f +* g) & y = (f +* g) . x ) by ; :: thesis: verum
end;
suppose A13: y in rng g ; :: thesis: ( x in dom (f +* g) & y = (f +* g) . x )
A14: ( dom (f ") = rng f & dom (g ") = rng g ) by FUNCT_1:33;
consider z being object such that
A15: z in dom g and
A16: y = g . z by ;
z = (g ") . y by ;
then z = ((g ") +* (f ")) . y by ;
then A17: z = x by ;
( dom (f +* g) = (dom f) \/ (dom g) & y = (g +* f) . z ) by ;
hence ( x in dom (f +* g) & y = (f +* g) . x ) by ; :: thesis: verum
end;
end;
end;
thus ( x in dom (f +* g) & y = (f +* g) . x implies ( y in rng (f +* g) & x = ((f ") +* (g ")) . y ) ) :: thesis: verum
proof
A18: dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def 1;
assume that
A19: x in dom (f +* g) and
A20: y = (f +* g) . x ; :: thesis: ( y in rng (f +* g) & x = ((f ") +* (g ")) . y )
per cases ( x in dom f or x in dom g ) by ;
suppose A21: x in dom f ; :: thesis: ( y in rng (f +* g) & x = ((f ") +* (g ")) . y )
then not x in dom g by ;
then A22: y = f . x by ;
then A23: x = (f ") . y by ;
A24: ( dom (f ") = rng f & dom (g ") = rng g ) by FUNCT_1:33;
A25: y in rng f by ;
then y in (rng f) \/ (rng g) by XBOOLE_0:def 3;
hence ( y in rng (f +* g) & x = ((f ") +* (g ")) . y ) by ; :: thesis: verum
end;
suppose A26: x in dom g ; :: thesis: ( y in rng (f +* g) & x = ((f ") +* (g ")) . y )
then A27: y = g . x by ;
then A28: y in rng g by ;
then A29: y in (rng f) \/ (rng g) by XBOOLE_0:def 3;
A30: ( dom (f ") = rng f & dom (g ") = rng g ) by FUNCT_1:33;
x = (g ") . y by ;
then x = ((g ") +* (f ")) . y by ;
hence ( y in rng (f +* g) & x = ((f ") +* (g ")) . y ) by ; :: thesis: verum
end;
end;
end;
end;
dom ((f ") +* (g ")) = (dom (f ")) \/ (dom (g ")) by FUNCT_4:def 1
.= (rng f) \/ (dom (g ")) by FUNCT_1:33
.= (rng f) \/ (rng g) by FUNCT_1:33
.= rng (f +* g) by ;
hence (f +* g) " = (f ") +* (g ") by ; :: thesis: verum