let D, E be non empty set ; :: thesis: for p, q being FinSequence of D
for h being Function of D,E holds h * (p ^ q) = (h * p) ^ (h * q)
let p, q be FinSequence of D; :: thesis: for h being Function of D,E holds h * (p ^ q) = (h * p) ^ (h * q)
let h be Function of D,E; :: thesis: h * (p ^ q) = (h * p) ^ (h * q)
defpred S₁[ FinSequence of D] means h * (p ^ $1) = (h * p) ^ (h * $1);
A1: 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 A2: h * (p ^ q) = (h * p) ^ (h * q) ; :: thesis: S₁[q ^ <*d*>]
thus h * (p ^ (q ^ <*d*>)) = h * ((p ^ q) ^ <*d*>) by FINSEQ_1:32
.= (h * (p ^ q)) ^ <*(h . d)*> by Th8
.= (h * p) ^ ((h * q) ^ <*(h . d)*>) by A2, FINSEQ_1:32
.= (h * p) ^ (h * (q ^ <*d*>)) by Th8 ; :: thesis: verum

end;

h * (p ^ (<*> D)) = h * p by FINSEQ_1:34
.= (h * p) ^ (h * (<*> D)) by FINSEQ_1:34 ;
then A3: S₁[ <*> D] ;
for q being FinSequence of D holds S₁[q] from FINSEQ_2:sch 2(A3, A1);
hence h * (p ^ q) = (h * p) ^ (h * q) ; :: thesis: verum