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 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 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 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 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 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 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 S1[ FinSequence of D] means h . (F "**" \$1) = H "**" (h * \$1);
A5: 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 A6: h . (F "**" q) = H "**" (h * q) ; :: thesis: S1[q ^ <*d*>]
thus h . (F "**" (q ^ <*d*>)) = h . (F . ((F "**" q),d)) by
.= H . ((H "**" (h * q)),(h . d)) by A4, A6
.= H "**" ((h * q) ^ <*(h . d)*>) by
.= H "**" (h * (q ^ <*d*>)) by FINSEQOP:8 ; :: thesis: verum
end;
h . (F "**" (<*> D)) = h . () by
.= H "**" (<*> E) by
.= H "**" (h * (<*> D)) ;
then A7: S1[ <*> D] ;
for q being FinSequence of D holds S1[q] from hence h . (F "**" p) = H "**" (h * p) ; :: thesis: verum