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 S1[ 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 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: h * (p ^ q) = (h * p) ^ (h * q) ; :: thesis: S1[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
.= (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: S1[ <*> D] ;
for q being FinSequence of D holds S1[q] from hence h * (p ^ q) = (h * p) ^ (h * q) ; :: thesis: verum