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 (Shift J,n) = { (m + n) where m is Element of NAT : m in dom J } by Def12;

A2: 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 A3: 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 A4: 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 A1;
hence ((Shift I,n) +* (Shift J,n)) . (m + n) = (Shift J,n) . (m + n) by FUNCT_4:14
.= J . m by A4, Def12
.= (I +* J) . m by A4, FUNCT_4:14 ;
:: thesis: verum

end;

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

m in (dom I) \/ (dom J) by A3, FUNCT_4:def 1;
then A6: m in dom I by A5, XBOOLE_0:def 3;
for l being Element of NAT holds
( not m + n = l + n or not l in dom J ) by A5;
then not m + n in dom (Shift J,n) by A1;
hence ((Shift I,n) +* (Shift J,n)) . (m + n) = (Shift I,n) . (m + n) by FUNCT_4:12
.= I . m by A6, Def12
.= (I +* J) . m by A5, FUNCT_4:12 ;
:: thesis: verum

end;

end;

end;

A7: dom (Shift I,n) = { (m + n) where m is Element of NAT : m in dom I } by Def12;
A8: (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
A9: ( ( x = m + n & m in dom J ) or ( x = m + n & m in dom I ) ) by A1, A7;
m in (dom I) \/ (dom J) by A9, XBOOLE_0:def 3;
hence x in { (l + n) where l is Element of NAT : l in (dom I) \/ (dom J) } by A9; :: 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
A10: x = m + n and
A11: m in (dom I) \/ (dom J) ;
( m in dom I or m in dom J ) by A11, XBOOLE_0:def 3;
then ( x in dom (Shift I,n) or x in dom (Shift J,n) ) by A1, A7, A10;
hence x in (dom (Shift I,n)) \/ (dom (Shift J,n)) by XBOOLE_0:def 3; :: thesis: verum

end;

dom (I +* J) = (dom I) \/ (dom J) by FUNCT_4:def 1;
then dom ((Shift I,n) +* (Shift J,n)) = { (m + n) where m is Element of NAT : m in dom (I +* J) } by A8, FUNCT_4:def 1;
hence Shift (I +* J),n = (Shift I,n) +* (Shift J,n) by A2, Def12; :: thesis: verum