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:8;
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:56 ;
A3: 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:56 ;
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 ;
k in dom (X ^ <*y*>) by A4, Def10;
then A5: (FinSeqM x,(X ^ <*y*>)) . k = (MemberFunc ((X ^ <*y*>) . k),A) . x by Def10;
A6: k <= (len X) + 1 by A2, A4, FINSEQ_1:3;
A7: 1 <= k by A4, FINSEQ_3:27;

per cases ( k <= len X or k = (len X) + 1 ) by A6, 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 A7, FINSEQ_3:27;
k in dom (FinSeqM x,X) by A1, A7, A8, FINSEQ_3:27;
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 A5, 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:59;
hence (FinSeqM x,(X ^ <*y*>)) . k = ((FinSeqM x,X) ^ <*((MemberFunc y,A) . x)*>) . k by A5, A10, FINSEQ_1:59; :: thesis: verum

end;

end;

end;

hence FinSeqM x,(X ^ <*y*>) = (FinSeqM x,X) ^ <*((MemberFunc y,A) . x)*> by A2, A3, FINSEQ_1:17; :: thesis: verum