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