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

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 ex m being Element of NAT st
( x = m -' 1 & m in dom p ) by A3;
hence x in dom (Load (p ^ q)) by A2, A1; :: thesis: verum

end;

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

A5: now

A6: dom p c= dom (p ^ q) by FINSEQ_1:39;
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: k + 1 in dom p by A7, Th26;
thus (Load (p ^ q)) . k = (p ^ q) /. (k + 1) by A4, A7, Def1
.= (p ^ q) . (k + 1) by A6, A8, PARTFUN1:def 8
.= p . (k + 1) by A8, FINSEQ_1:def 7
.= p /. (k + 1) by A8, 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 A9: 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 A5, A9; :: thesis: verum

end;

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