let D', E, D be non empty set ; :: thesis: for d' being Element of D'
for F being Function of [:D,D':],E
for p, q being FinSequence of D holds F [:] (p ^ q),d' = (F [:] p,d') ^ (F [:] q,d')
let d' be Element of D'; :: thesis: for F being Function of [:D,D':],E
for p, q being FinSequence of D holds F [:] (p ^ q),d' = (F [:] p,d') ^ (F [:] q,d')
let F be Function of [:D,D':],E; :: thesis: for p, q being FinSequence of D holds F [:] (p ^ q),d' = (F [:] p,d') ^ (F [:] q,d')
let p, q be FinSequence of D; :: thesis: F [:] (p ^ q),d' = (F [:] p,d') ^ (F [:] q,d')
defpred S1[ FinSequence of D] means F [:] (p ^ $1),d' = (F [:] p,d') ^ (F [:] $1,d');
F [:] (p ^ (<*> D)),d' =
F [:] p,d'
by FINSEQ_1:47
.=
(F [:] p,d') ^ (<*> E)
by FINSEQ_1:47
.=
(F [:] p,d') ^ (F [:] (<*> D),d')
by FINSEQ_2:99
;
then A1:
S1[ <*> D]
;
A2:
for q being FinSequence of D
for d being Element of D st S1[q] holds
S1[q ^ <*d*>]
proof
let q be
FinSequence of
D;
:: thesis: for d being Element of D st S1[q] holds
S1[q ^ <*d*>]let d be
Element of
D;
:: thesis: ( S1[q] implies S1[q ^ <*d*>] )
assume A3:
F [:] (p ^ q),
d' = (F [:] p,d') ^ (F [:] q,d')
;
:: thesis: S1[q ^ <*d*>]
thus F [:] (p ^ (q ^ <*d*>)),
d' =
F [:] ((p ^ q) ^ <*d*>),
d'
by FINSEQ_1:45
.=
(F [:] (p ^ q),d') ^ <*(F . d,d')*>
by Th15
.=
(F [:] p,d') ^ ((F [:] q,d') ^ <*(F . d,d')*>)
by A3, FINSEQ_1:45
.=
(F [:] p,d') ^ (F [:] (q ^ <*d*>),d')
by Th15
;
:: thesis: verum
end;
for q being FinSequence of D holds S1[q]
from FINSEQ_2:sch 2(A1, A2);
hence
F [:] (p ^ q),d' = (F [:] p,d') ^ (F [:] q,d')
; :: thesis: verum