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

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