let A be finite Approximation_Space; 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; 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; for y being Subset of A holds FinSeqM (x,(X ^ <*y*>)) = (FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*>
let y be Subset of A; 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;
( 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*>)))
;
(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
;
(FinSeqM (x,(X ^ <*y*>))) . k = ((FinSeqM (x,X)) ^ <*((MemberFunc (y,A)) . x)*>) . kthen 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;
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; verum