let s, f be Function; :: thesis: for n being Nat holds Shift ((f * s),n) = f * (Shift (s,n))
let n be Nat; :: thesis: Shift ((f * s),n) = f * (Shift (s,n))
A1: dom (f * s) c= dom s by RELAT_1:25;
A2: dom (Shift (s,n)) = { (m + n) where m is Nat : m in dom s } by Def12;

now :: thesis: for e being object holds
( ( e in { (m + n) where m is Nat : m in dom (f * s) } implies ( e in dom (Shift (s,n)) & (Shift (s,n)) . e in dom f ) ) & ( e in dom (Shift (s,n)) & (Shift (s,n)) . e in dom f implies e in { (m + n) where m is Nat : m in dom (f * s) } ) )

let e be object ; :: thesis: ( ( e in { (m + n) where m is Nat : m in dom (f * s) } implies ( e in dom (Shift (s,n)) & (Shift (s,n)) . e in dom f ) ) & ( e in dom (Shift (s,n)) & (Shift (s,n)) . e in dom f implies e in { (m + n) where m is Nat : m in dom (f * s) } ) )
thus ( e in { (m + n) where m is Nat : m in dom (f * s) } implies ( e in dom (Shift (s,n)) & (Shift (s,n)) . e in dom f ) ) :: thesis: ( e in dom (Shift (s,n)) & (Shift (s,n)) . e in dom f implies e in { (m + n) where m is Nat : m in dom (f * s) } )

proof

assume e in { (m + n) where m is Nat : m in dom (f * s) } ; :: thesis: ( e in dom (Shift (s,n)) & (Shift (s,n)) . e in dom f )
then consider m being Nat such that
A3: e = m + n and
A4: m in dom (f * s) ;
thus e in dom (Shift (s,n)) by A2, A1, A3, A4; :: thesis: (Shift (s,n)) . e in dom f
(Shift (s,n)) . e = s . m by A1, A3, A4, Def12;
hence (Shift (s,n)) . e in dom f by A4, FUNCT_1:11; :: thesis: verum

end;

assume e in dom (Shift (s,n)) ; :: thesis: ( (Shift (s,n)) . e in dom f implies e in { (m + n) where m is Nat : m in dom (f * s) } )
then consider m0 being Nat such that
A5: e = m0 + n and
A6: m0 in dom s by A2;
assume (Shift (s,n)) . e in dom f ; :: thesis: e in { (m + n) where m is Nat : m in dom (f * s) }
then s . m0 in dom f by A5, A6, Def12;
then m0 in dom (f * s) by A6, FUNCT_1:11;
hence e in { (m + n) where m is Nat : m in dom (f * s) } by A5; :: thesis: verum

end;

then (Shift (s,n)) " (dom f) = { (m + n) where m is Nat : m in dom (f * s) } by FUNCT_1:def 7;
then A7: dom (f * (Shift (s,n))) = { (m + n) where m is Nat : m in dom (f * s) } by RELAT_1:147;

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

let m be Nat; :: thesis: ( m in dom (f * s) implies (f * (Shift (s,n))) . (m + n) = (f * s) . m )
assume A8: m in dom (f * s) ; :: thesis: (f * (Shift (s,n))) . (m + n) = (f * s) . m
then m + n in dom (Shift (s,n)) by A2, A1;
hence (f * (Shift (s,n))) . (m + n) = f . ((Shift (s,n)) . (m + n)) by FUNCT_1:13
.= f . (s . m) by A1, A8, Def12
.= (f * s) . m by A8, FUNCT_1:12 ;
:: thesis: verum

end;

hence Shift ((f * s),n) = f * (Shift (s,n)) by A7, Def12; :: thesis: verum