let E, D 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₁[ FinSequence of D] means h . (F "**" $1) = H "**" (h * $1);
h . (F "**" (<*> D)) = h . (the_unity_wrt F) by A1, FINSOP_1:11
.= H "**" (<*> E) by A2, A3, FINSOP_1:11
.= H "**" (h * (<*> D)) by RELAT_1:62 ;
then A5: S₁[ <*> D] ;
A6: 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 A7: h . (F "**" q) = H "**" (h * q) ; :: thesis: S₁[q ^ <*d*>]
thus h . (F "**" (q ^ <*d*>)) = h . (F . (F "**" q),d) by A1, FINSOP_1:5
.= H . (H "**" (h * q)),(h . d) by A4, A7
.= H "**" ((h * q) ^ <*(h . d)*>) by A2, FINSOP_1:5
.= H "**" (h * (q ^ <*d*>)) by FINSEQOP:9 ; :: thesis: verum

end;

for q being FinSequence of D holds S₁[q] from FINSEQ_2:sch 2(A5, A6);
hence h . (F "**" p) = H "**" (h * p) ; :: thesis: verum