let n be Element of NAT ; :: thesis: for I, J being Function holds Shift (I +* J),n = (Shift I,n) +* (Shift J,n)
let I, J be Function; :: thesis: Shift (I +* J),n = (Shift I,n) +* (Shift J,n)
A1: dom (I +* J) = (dom I) \/ (dom J) by FUNCT_4:def 1;
A2: dom (Shift J,n) = { (m + n) where m is Element of NAT : m in dom J } by Def12;
A3: dom (Shift I,n) = { (m + n) where m is Element of NAT : m in dom I } by Def12;
(dom (Shift I,n)) \/ (dom (Shift J,n)) = { (m + n) where m is Element of NAT : m in (dom I) \/ (dom J) }

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { (m + n) where m is Element of NAT : m in (dom I) \/ (dom J) } c= (dom (Shift I,n)) \/ (dom (Shift J,n))

let x be set ; :: thesis: ( x in (dom (Shift I,n)) \/ (dom (Shift J,n)) implies x in { (l + n) where l is Element of NAT : l in (dom I) \/ (dom J) } )
assume x in (dom (Shift I,n)) \/ (dom (Shift J,n)) ; :: thesis: x in { (l + n) where l is Element of NAT : l in (dom I) \/ (dom J) }
then ( x in dom (Shift I,n) or x in dom (Shift J,n) ) by XBOOLE_0:def 3;
then consider m being Element of NAT such that
A4: ( ( x = m + n & m in dom J ) or ( x = m + n & m in dom I ) ) by A2, A3;
m in (dom I) \/ (dom J) by A4, XBOOLE_0:def 3;
hence x in { (l + n) where l is Element of NAT : l in (dom I) \/ (dom J) } by A4; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (m + n) where m is Element of NAT : m in (dom I) \/ (dom J) } or x in (dom (Shift I,n)) \/ (dom (Shift J,n)) )
assume x in { (m + n) where m is Element of NAT : m in (dom I) \/ (dom J) } ; :: thesis: x in (dom (Shift I,n)) \/ (dom (Shift J,n))
then consider m being Element of NAT such that
A5: x = m + n and
A6: m in (dom I) \/ (dom J) ;
( m in dom I or m in dom J ) by A6, XBOOLE_0:def 3;
then ( x in dom (Shift I,n) or x in dom (Shift J,n) ) by A2, A3, A5;
hence x in (dom (Shift I,n)) \/ (dom (Shift J,n)) by XBOOLE_0:def 3; :: thesis: verum

end;

then A7: dom ((Shift I,n) +* (Shift J,n)) = { (m + n) where m is Element of NAT : m in dom (I +* J) } by A1, FUNCT_4:def 1;

now

let m be Element of NAT ; :: thesis: ( m in dom (I +* J) implies ((Shift I,n) +* (Shift J,n)) . (b₁ + n) = (I +* J) . b₁ )
assume A8: m in dom (I +* J) ; :: thesis: ((Shift I,n) +* (Shift J,n)) . (b₁ + n) = (I +* J) . b₁

per cases ( m in dom J or not m in dom J ) ;

suppose A9: m in dom J ; :: thesis: ((Shift I,n) +* (Shift J,n)) . (b₁ + n) = (I +* J) . b₁

then m + n in dom (Shift J,n) by A2;
hence ((Shift I,n) +* (Shift J,n)) . (m + n) = (Shift J,n) . (m + n) by FUNCT_4:14
.= J . m by A9, Def12
.= (I +* J) . m by A9, FUNCT_4:14 ;
:: thesis: verum

end;

suppose A10: not m in dom J ; :: thesis: ((Shift I,n) +* (Shift J,n)) . (b₁ + n) = (I +* J) . b₁

then for l being Element of NAT holds
( not m + n = l + n or not l in dom J ) ;
then A11: not m + n in dom (Shift J,n) by A2;
m in (dom I) \/ (dom J) by A8, FUNCT_4:def 1;
then A12: m in dom I by A10, XBOOLE_0:def 3;
thus ((Shift I,n) +* (Shift J,n)) . (m + n) = (Shift I,n) . (m + n) by A11, FUNCT_4:12
.= I . m by A12, Def12
.= (I +* J) . m by A10, FUNCT_4:12 ; :: thesis: verum

end;

end;

end;

hence Shift (I +* J),n = (Shift I,n) +* (Shift J,n) by A7, Def12; :: thesis: verum