let n, m be Nat; :: thesis: for I being Function holds Shift ((Shift (I,m)),n) = Shift (I,(m + n))
let I be Function; :: thesis: Shift ((Shift (I,m)),n) = Shift (I,(m + n))
set A = { (l + m) where l is Nat : l in dom I } ;
A1: dom (Shift (I,m)) = { (l + m) where l is Nat : l in dom I } by Def12;
A2: now :: thesis: for l being Nat st l in dom I holds
(Shift ((Shift (I,m)),n)) . (l + (m + n)) = I . l
let l be Nat; :: thesis: ( l in dom I implies (Shift ((Shift (I,m)),n)) . (l + (m + n)) = I . l )
assume A3: l in dom I ; :: thesis: (Shift ((Shift (I,m)),n)) . (l + (m + n)) = I . l
then A4: l + m in dom (Shift (I,m)) by A1;
thus (Shift ((Shift (I,m)),n)) . (l + (m + n)) = (Shift ((Shift (I,m)),n)) . ((l + m) + n)
.= (Shift (I,m)) . (l + m) by A4, Def12
.= I . l by A3, Def12 ; :: thesis: verum
end;
{ (p + n) where p is Nat : p in { (l + m) where l is Nat : l in dom I } } = { (q + (m + n)) where q is Nat : q in dom I }
proof
thus { (p + n) where p is Nat : p in { (l + m) where l is Nat : l in dom I } } c= { (q + (m + n)) where q is Nat : q in dom I } :: according to XBOOLE_0:def 10 :: thesis: { (q + (m + n)) where q is Nat : q in dom I } c= { (p + n) where p is Nat : p in { (l + m) where l is Nat : l in dom I } }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (p + n) where p is Nat : p in { (l + m) where l is Nat : l in dom I } } or x in { (q + (m + n)) where q is Nat : q in dom I } )
assume x in { (p + n) where p is Nat : p in { (l + m) where l is Nat : l in dom I } } ; :: thesis: x in { (q + (m + n)) where q is Nat : q in dom I }
then consider p being Nat such that
A5: x = p + n and
A6: p in { (l + m) where l is Nat : l in dom I } ;
consider l being Nat such that
A7: p = l + m and
A8: l in dom I by A6;
x = l + (m + n) by A5, A7;
hence x in { (q + (m + n)) where q is Nat : q in dom I } by A8; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (q + (m + n)) where q is Nat : q in dom I } or x in { (p + n) where p is Nat : p in { (l + m) where l is Nat : l in dom I } } )
assume x in { (q + (m + n)) where q is Nat : q in dom I } ; :: thesis: x in { (p + n) where p is Nat : p in { (l + m) where l is Nat : l in dom I } }
then consider q being Nat such that
A9: ( x = q + (m + n) & q in dom I ) ;
( x = (q + m) + n & q + m in { (l + m) where l is Nat : l in dom I } ) by A9;
hence x in { (p + n) where p is Nat : p in { (l + m) where l is Nat : l in dom I } } ; :: thesis: verum
end;
then dom (Shift ((Shift (I,m)),n)) = { (l + (m + n)) where l is Nat : l in dom I } by A1, Def12;
hence Shift ((Shift (I,m)),n) = Shift (I,(m + n)) by A2, Def12; :: thesis: verum