let a be Domain-Sequence; :: thesis: for u being UnOps of a
for f being Element of product a
for i being Element of dom a holds ((Frege u) . f) . i = (u . i) . (f . i)
let u be UnOps of a; :: thesis: for f being Element of product a
for i being Element of dom a holds ((Frege u) . f) . i = (u . i) . (f . i)
let f be Element of product a; :: thesis: for i being Element of dom a holds ((Frege u) . f) . i = (u . i) . (f . i)
let i be Element of dom a; :: thesis: ((Frege u) . f) . i = (u . i) . (f . i)
A1: ( dom u = Seg (len u) & doms u = a ) by Th14, FINSEQ_1:def 3;
( dom a = Seg (len a) & len a = len u ) by Th12, FINSEQ_1:def 3;
hence ((Frege u) . f) . i = (u . i) . (f . i) by A1, FUNCT_6:37; :: thesis: verum