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₁[ 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₁[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 A6: h . (F "**" q) = H "**" (h * q) ; :: thesis: S₁[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;

h . (F "**" (<*> D)) = h . (the_unity_wrt F) by A1, FINSOP_1:10
.= H "**" (<*> E) by A2, A3, FINSOP_1:10
.= H "**" (h * (<*> D)) ;
then A7: S₁[ <*> D] ;
for q being FinSequence of D holds S₁[q] from FINSEQ_2:sch 2(A7, A5);
hence h . (F "**" p) = H "**" (h * p) ; :: thesis: verum