let p, q be FinSequence of the Instructions of SCM+FSA ; :: thesis: Load p c= Load (p ^ q)
A1: dom (Load p) = { (m -' 1) where m is Element of NAT : m in dom p } by Def1;
A2: dom (Load (p ^ q)) = { (m -' 1) where m is Element of NAT : m in dom (p ^ q) } by Def1;
A3: dom p c= dom (p ^ q) by FINSEQ_1:39;

now

let x be set ; :: thesis: ( x in dom (Load p) implies x in dom (Load (p ^ q)) )
assume x in dom (Load p) ; :: thesis: x in dom (Load (p ^ q))
then consider m being Element of NAT such that
A4: ( x = m -' 1 & m in dom p ) by A1;
thus x in dom (Load (p ^ q)) by A2, A3, A4; :: thesis: verum

end;

then A5: dom (Load p) c= dom (Load (p ^ q)) by TARSKI:def 3;

A6: now

let k be Element of NAT ; :: thesis: ( k in dom (Load p) implies (Load (p ^ q)) . k = (Load p) . k )
assume A7: k in dom (Load p) ; :: thesis: (Load (p ^ q)) . k = (Load p) . k
A8: dom p c= dom (p ^ q) by FINSEQ_1:39;
A9: k + 1 in dom p by A7, Th26;
thus (Load (p ^ q)) . k = (p ^ q) /. (k + 1) by A5, A7, Def1
.= (p ^ q) . (k + 1) by A8, A9, PARTFUN1:def 8
.= p . (k + 1) by A9, FINSEQ_1:def 7
.= p /. (k + 1) by A9, PARTFUN1:def 8
.= (Load p) . k by A7, Def1 ; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in dom (Load p) implies (Load p) . x = (Load (p ^ q)) . x )
assume A10: x in dom (Load p) ; :: thesis: (Load p) . x = (Load (p ^ q)) . x
then x in { (m -' 1) where m is Element of NAT : m in dom p } by Def1;
then ex m being Element of NAT st
( x = m -' 1 & m in dom p ) ;
hence (Load p) . x = (Load (p ^ q)) . x by A6, A10; :: thesis: verum

end;

hence Load p c= Load (p ^ q) by A5, GRFUNC_1:8; :: thesis: verum