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_{1}[ 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_{1}[q] holds

S_{1}[q ^ <*d*>]

.= (h * p) ^ (h * (<*> D)) by FINSEQ_1:34 ;

then A3: S_{1}[ <*> D]
;

for q being FinSequence of D holds S_{1}[q]
from FINSEQ_2:sch 2(A3, A1);

hence h * (p ^ q) = (h * p) ^ (h * q) ; :: thesis: verum

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

A1: for q being FinSequence of D

for d being Element of D st S

S

proof

h * (p ^ (<*> D)) =
h * p
by FINSEQ_1:34
let q be FinSequence of D; :: thesis: for d being Element of D st S_{1}[q] holds

S_{1}[q ^ <*d*>]

let d be Element of D; :: thesis: ( S_{1}[q] implies S_{1}[q ^ <*d*>] )

assume A2: h * (p ^ q) = (h * p) ^ (h * q) ; :: thesis: S_{1}[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;S

let d be Element of D; :: thesis: ( S

assume A2: h * (p ^ q) = (h * p) ^ (h * q) ; :: thesis: S

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

.= (h * p) ^ (h * (<*> D)) by FINSEQ_1:34 ;

then A3: S

for q being FinSequence of D holds S

hence h * (p ^ q) = (h * p) ^ (h * q) ; :: thesis: verum