let I, J be Function; :: thesis: for n being Nat holds Shift ((I +* J),n) = (Shift (I,n)) +* (Shift (J,n))
let n be Nat; :: thesis: Shift ((I +* J),n) = (Shift (I,n)) +* (Shift (J,n))
A1: dom (Shift (J,n)) = { (m + n) where m is Nat : m in dom J } by Def12;

A2: now :: thesis: for m being Nat st m in dom (I +* J) holds
((Shift (I,n)) +* (Shift (J,n))) . (m + n) = (I +* J) . m

let m be 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:13
.= J . m by A4, Def12
.= (I +* J) . m by A4, FUNCT_4:13 ;
:: 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 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:11
.= I . m by A6, Def12
.= (I +* J) . m by A5, FUNCT_4:11 ;
:: thesis: verum

end;

end;

end;

A7: dom (Shift (I,n)) = { (m + n) where m is Nat : m in dom I } by Def12;
A8: (dom (Shift (I,n))) \/ (dom (Shift (J,n))) = { (m + n) where m is Nat : m in (dom I) \/ (dom J) }

proof

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

let x be object ; :: thesis: ( x in (dom (Shift (I,n))) \/ (dom (Shift (J,n))) implies x in { (l + n) where l is 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 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 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 Nat : l in (dom I) \/ (dom J) } by A9; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (m + n) where m is 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 Nat : m in (dom I) \/ (dom J) } ; :: thesis: x in (dom (Shift (I,n))) \/ (dom (Shift (J,n)))
then consider m being 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 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