let D, E be non empty set ; :: thesis: for F being BinOp of D

for H being BinOp of E

for h being Function of D,E

for p being FinSequence of D st F is having_a_unity & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds

h . (F "**" p) = H "**" (h * p)

let F be BinOp of D; :: thesis: for H being BinOp of E

for h being Function of D,E

for p being FinSequence of D st F is having_a_unity & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds

h . (F "**" p) = H "**" (h * p)

let H be BinOp of E; :: thesis: for h being Function of D,E

for p being FinSequence of D st F is having_a_unity & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds

h . (F "**" p) = H "**" (h * p)

let h be Function of D,E; :: thesis: for p being FinSequence of D st F is having_a_unity & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds

h . (F "**" p) = H "**" (h * p)

let p be FinSequence of D; :: thesis: ( F is having_a_unity & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) implies h . (F "**" p) = H "**" (h * p) )

assume that

A1: F is having_a_unity and

A2: H is having_a_unity and

A3: h . (the_unity_wrt F) = the_unity_wrt H and

A4: for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ; :: thesis: h . (F "**" p) = H "**" (h * p)

defpred S_{1}[ FinSequence of D] means h . (F "**" $1) = H "**" (h * $1);

A5: for q being FinSequence of D

for d being Element of D st S_{1}[q] holds

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

.= H "**" (<*> E) by A2, A3, FINSOP_1:10

.= H "**" (h * (<*> D)) ;

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

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

hence h . (F "**" p) = H "**" (h * p) ; :: thesis: verum

for H being BinOp of E

for h being Function of D,E

for p being FinSequence of D st F is having_a_unity & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds

h . (F "**" p) = H "**" (h * p)

let F be BinOp of D; :: thesis: for H being BinOp of E

for h being Function of D,E

for p being FinSequence of D st F is having_a_unity & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds

h . (F "**" p) = H "**" (h * p)

let H be BinOp of E; :: thesis: for h being Function of D,E

for p being FinSequence of D st F is having_a_unity & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds

h . (F "**" p) = H "**" (h * p)

let h be Function of D,E; :: thesis: for p being FinSequence of D st F is having_a_unity & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) holds

h . (F "**" p) = H "**" (h * p)

let p be FinSequence of D; :: thesis: ( F is having_a_unity & H is having_a_unity & h . (the_unity_wrt F) = the_unity_wrt H & ( for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ) implies h . (F "**" p) = H "**" (h * p) )

assume that

A1: F is having_a_unity and

A2: H is having_a_unity and

A3: h . (the_unity_wrt F) = the_unity_wrt H and

A4: for d1, d2 being Element of D holds h . (F . (d1,d2)) = H . ((h . d1),(h . d2)) ; :: thesis: h . (F "**" p) = H "**" (h * p)

defpred S

A5: for q being FinSequence of D

for d being Element of D st S

S

proof

h . (F "**" (<*> D)) =
h . (the_unity_wrt F)
by A1, FINSOP_1:10
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 A6: h . (F "**" q) = H "**" (h * q) ; :: thesis: S_{1}[q ^ <*d*>]

thus h . (F "**" (q ^ <*d*>)) = h . (F . ((F "**" q),d)) by A1, FINSOP_1:4

.= H . ((H "**" (h * q)),(h . d)) by A4, A6

.= H "**" ((h * q) ^ <*(h . d)*>) by A2, FINSOP_1:4

.= H "**" (h * (q ^ <*d*>)) by FINSEQOP:8 ; :: thesis: verum

end;S

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

assume A6: h . (F "**" q) = H "**" (h * q) ; :: thesis: S

thus h . (F "**" (q ^ <*d*>)) = h . (F . ((F "**" q),d)) by A1, FINSOP_1:4

.= H . ((H "**" (h * q)),(h . d)) by A4, A6

.= H "**" ((h * q) ^ <*(h . d)*>) by A2, FINSOP_1:4

.= H "**" (h * (q ^ <*d*>)) by FINSEQOP:8 ; :: thesis: verum

.= H "**" (<*> E) by A2, A3, FINSOP_1:10

.= H "**" (h * (<*> D)) ;

then A7: S

for q being FinSequence of D holds S

hence h . (F "**" p) = H "**" (h * p) ; :: thesis: verum