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 [;] d,(p' ^ q') = (F [;] d,p') ^ (F [;] d,q')
let d be Element of D; :: thesis: for F being Function of [:D,D':],E
for p', q' being FinSequence of D' holds F [;] d,(p' ^ q') = (F [;] d,p') ^ (F [;] d,q')
let F be Function of [:D,D':],E; :: thesis: for p', q' being FinSequence of D' holds F [;] d,(p' ^ q') = (F [;] d,p') ^ (F [;] d,q')
let p', q' be FinSequence of D'; :: thesis: F [;] d,(p' ^ q') = (F [;] d,p') ^ (F [;] d,q')
defpred S₁[ FinSequence of D'] means F [;] d,(p' ^ $1) = (F [;] d,p') ^ (F [;] d,$1);
F [;] d,(p' ^ (<*> D')) = F [;] d,p' by FINSEQ_1:47
.= (F [;] d,p') ^ (<*> E) by FINSEQ_1:47
.= (F [;] d,p') ^ (F [;] d,(<*> D')) by FINSEQ_2:93 ;
then A1: S₁[ <*> D'] ;
A2: for q' being FinSequence of D'
for d' being Element of D' st S₁[q'] holds
S₁[q' ^ <*d'*>]

proof

let q' be FinSequence of D'; :: thesis: for d' being Element of D' st S₁[q'] holds
S₁[q' ^ <*d'*>]
let d' be Element of D'; :: thesis: ( S₁[q'] implies S₁[q' ^ <*d'*>] )
assume A3: F [;] d,(p' ^ q') = (F [;] d,p') ^ (F [;] d,q') ; :: thesis: S₁[q' ^ <*d'*>]
thus F [;] d,(p' ^ (q' ^ <*d'*>)) = F [;] d,((p' ^ q') ^ <*d'*>) by FINSEQ_1:45
.= (F [;] d,(p' ^ q')) ^ <*(F . d,d')*> by Th13
.= (F [;] d,p') ^ ((F [;] d,q') ^ <*(F . d,d')*>) by A3, FINSEQ_1:45
.= (F [;] d,p') ^ (F [;] d,(q' ^ <*d'*>)) by Th13 ; :: thesis: verum

end;

for q' being FinSequence of D' holds S₁[q'] from FINSEQ_2:sch 2(A1, A2);
hence F [;] d,(p' ^ q') = (F [;] d,p') ^ (F [;] d,q') ; :: thesis: verum