let D, D9, E be non empty set ; :: thesis: for d9 being Element of D9
for F being Function of [:D,D9:],E
for p, q being FinSequence of D holds F [:] ((p ^ q),d9) = (F [:] (p,d9)) ^ (F [:] (q,d9))

let d9 be Element of D9; :: thesis: for F being Function of [:D,D9:],E
for p, q being FinSequence of D holds F [:] ((p ^ q),d9) = (F [:] (p,d9)) ^ (F [:] (q,d9))

let F be Function of [:D,D9:],E; :: thesis: for p, q being FinSequence of D holds F [:] ((p ^ q),d9) = (F [:] (p,d9)) ^ (F [:] (q,d9))
let p, q be FinSequence of D; :: thesis: F [:] ((p ^ q),d9) = (F [:] (p,d9)) ^ (F [:] (q,d9))
defpred S1[ FinSequence of D] means F [:] ((p ^ \$1),d9) = (F [:] (p,d9)) ^ (F [:] (\$1,d9));
A1: 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 A2: F [:] ((p ^ q),d9) = (F [:] (p,d9)) ^ (F [:] (q,d9)) ; :: thesis: S1[q ^ <*d*>]
thus F [:] ((p ^ (q ^ <*d*>)),d9) = F [:] (((p ^ q) ^ <*d*>),d9) by FINSEQ_1:32
.= (F [:] ((p ^ q),d9)) ^ <*(F . (d,d9))*> by Th14
.= (F [:] (p,d9)) ^ ((F [:] (q,d9)) ^ <*(F . (d,d9))*>) by
.= (F [:] (p,d9)) ^ (F [:] ((q ^ <*d*>),d9)) by Th14 ; :: thesis: verum
end;
F [:] ((p ^ (<*> D)),d9) = F [:] (p,d9) by FINSEQ_1:34
.= (F [:] (p,d9)) ^ (<*> E) by FINSEQ_1:34
.= (F [:] (p,d9)) ^ (F [:] ((<*> D),d9)) by FINSEQ_2:85 ;
then A3: S1[ <*> D] ;
for q being FinSequence of D holds S1[q] from hence F [:] ((p ^ q),d9) = (F [:] (p,d9)) ^ (F [:] (q,d9)) ; :: thesis: verum