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

now

let e be set ; :: thesis: ( ( e in { (m + n) where m is Element of 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 Element of NAT : m in dom (f * s) } ) )
thus ( e in { (m + n) where m is Element of 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 Element of NAT : m in dom (f * s) } )

proof

assume e in { (m + n) where m is Element of NAT : m in dom (f * s) } ; :: thesis: ( e in dom (Shift s,n) & (Shift s,n) . e in dom f )
then consider m being Element of 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:21; :: 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 Element of NAT : m in dom (f * s) } )
then consider m0 being Element of 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 Element of 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:21;
hence e in { (m + n) where m is Element of NAT : m in dom (f * s) } by A5; :: thesis: verum

end;

then (Shift s,n) " (dom f) = { (m + n) where m is Element of NAT : m in dom (f * s) } by FUNCT_1:def 13;
then A7: dom (f * (Shift s,n)) = { (m + n) where m is Element of NAT : m in dom (f * s) } by RELAT_1:182;

now

let m be Element of 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:23
.= f . (s . m) by A1, A8, Def12
.= (f * s) . m by A8, FUNCT_1:22 ;
:: thesis: verum

end;

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