let A be finite Approximation_Space; :: thesis: for X being FinSequence of bool the carrier of A
for x being Element of A
for y being Subset of A holds FinSeqM (x,(X ^ <*y*>)) = (FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*>
let X be FinSequence of bool the carrier of A; :: thesis: for x being Element of A
for y being Subset of A holds FinSeqM (x,(X ^ <*y*>)) = (FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*>
let x be Element of A; :: thesis: for y being Subset of A holds FinSeqM (x,(X ^ <*y*>)) = (FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*>
let y be Subset of A; :: thesis: FinSeqM (x,(X ^ <*y*>)) = (FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*>
set p = FinSeqM (x,(X ^ <*y*>));
set q = (FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*>;
dom X = dom (FinSeqM (x,X)) by Def10;
then Seg (len X) = dom (FinSeqM (x,X)) by FINSEQ_1:def 3
.= Seg (len (FinSeqM (x,X))) by FINSEQ_1:def 3 ;
then A1: len X = len (FinSeqM (x,X)) by FINSEQ_1:6;
A2: dom (FinSeqM (x,(X ^ <*y*>))) = dom (X ^ <*y*>) by Def10
.= Seg ((len X) + (len <*y*>)) by FINSEQ_1:def 7
.= Seg ((len X) + 1) by FINSEQ_1:39 ;
A3: for k being Nat st k in dom (FinSeqM (x,(X ^ <*y*>))) holds
(FinSeqM (x,(X ^ <*y*>))) . k = ((FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*>) . k

proof

let k be Nat; :: thesis: ( k in dom (FinSeqM (x,(X ^ <*y*>))) implies (FinSeqM (x,(X ^ <*y*>))) . k = ((FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*>) . k )
assume A4: k in dom (FinSeqM (x,(X ^ <*y*>))) ; :: thesis: (FinSeqM (x,(X ^ <*y*>))) . k = ((FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*>) . k
then reconsider k = k as Element of NAT ;
A5: 1 <= k by A4, FINSEQ_3:25;
k in dom (X ^ <*y*>) by A4, Def10;
then A6: (FinSeqM (x,(X ^ <*y*>))) . k = (MemberFunc (((X ^ <*y*>) . k),A)) . x by Def10;
A7: k <= (len X) + 1 by A2, A4, FINSEQ_1:1;

per cases ( k <= len X or k = (len X) + 1 ) by A7, NAT_1:8;

suppose A8: k <= len X ; :: thesis: (FinSeqM (x,(X ^ <*y*>))) . k = ((FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*>) . k

then A9: k in dom X by A5, FINSEQ_3:25;
k in dom (FinSeqM (x,X)) by A1, A5, A8, FINSEQ_3:25;
then ((FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*>) . k = (FinSeqM (x,X)) . k by FINSEQ_1:def 7
.= (MemberFunc ((X . k),A)) . x by A9, Def10 ;
hence (FinSeqM (x,(X ^ <*y*>))) . k = ((FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*>) . k by A6, A9, FINSEQ_1:def 7; :: thesis: verum

end;

suppose A10: k = (len X) + 1 ; :: thesis: (FinSeqM (x,(X ^ <*y*>))) . k = ((FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*>) . k

then ((FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*>) . k = (MemberFunc (y,A)) . x by A1, FINSEQ_1:42;
hence (FinSeqM (x,(X ^ <*y*>))) . k = ((FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*>) . k by A6, A10, FINSEQ_1:42; :: thesis: verum

end;

end;

end;

dom ((FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*>) = Seg ((len (FinSeqM (x,X))) + (len <*((MemberFunc (y,A)) . x)*>)) by FINSEQ_1:def 7
.= Seg ((len X) + 1) by A1, FINSEQ_1:39 ;
hence FinSeqM (x,(X ^ <*y*>)) = (FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*> by A2, A3, FINSEQ_1:13; :: thesis: verum