let n be Nat; :: thesis: for D being non empty set
for A being BinOp of D
for f being FinSequence of D
for F1 being finite set
for E1 being Enumeration of F1 st n in dom f holds
(len E1) |-> n in doms ((SignGenOp (f,A,F1)) * E1)
let D be non empty set ; :: thesis: for A being BinOp of D
for f being FinSequence of D
for F1 being finite set
for E1 being Enumeration of F1 st n in dom f holds
(len E1) |-> n in doms ((SignGenOp (f,A,F1)) * E1)
let A be BinOp of D; :: thesis: for f being FinSequence of D
for F1 being finite set
for E1 being Enumeration of F1 st n in dom f holds
(len E1) |-> n in doms ((SignGenOp (f,A,F1)) * E1)
let f be FinSequence of D; :: thesis: for F1 being finite set
for E1 being Enumeration of F1 st n in dom f holds
(len E1) |-> n in doms ((SignGenOp (f,A,F1)) * E1)
let F1 be finite set ; :: thesis: for E1 being Enumeration of F1 st n in dom f holds
(len E1) |-> n in doms ((SignGenOp (f,A,F1)) * E1)
let E1 be Enumeration of F1; :: thesis: ( n in dom f implies (len E1) |-> n in doms ((SignGenOp (f,A,F1)) * E1) )
assume A1: n in dom f ; :: thesis: (len E1) |-> n in doms ((SignGenOp (f,A,F1)) * E1)
set CE = (SignGenOp (f,A,F1)) * E1;
set s = (len E1) |-> n;
A2: ( len ((SignGenOp (f,A,F1)) * E1) = len E1 & len E1 = len ((len E1) |-> n) ) by CARD_1:def 7;
then A3: ( dom ((len E1) |-> n) = dom E1 & dom E1 = dom ((SignGenOp (f,A,F1)) * E1) ) by FINSEQ_3:29;
for i being Nat st i in dom ((len E1) |-> n) holds
((len E1) |-> n) . i in dom (((SignGenOp (f,A,F1)) * E1) . i)

proof

let i be Nat; :: thesis: ( i in dom ((len E1) |-> n) implies ((len E1) |-> n) . i in dom (((SignGenOp (f,A,F1)) * E1) . i) )
assume A4: i in dom ((len E1) |-> n) ; :: thesis: ((len E1) |-> n) . i in dom (((SignGenOp (f,A,F1)) * E1) . i)
( ((len E1) |-> n) . i = n & dom f = dom (SignGen (f,A,(E1 . i))) ) by Def11, A4, FINSEQ_2:57;
hence ((len E1) |-> n) . i in dom (((SignGenOp (f,A,F1)) * E1) . i) by A1, A3, A4, Th80; :: thesis: verum

end;

hence (len E1) |-> n in doms ((SignGenOp (f,A,F1)) * E1) by Th47, A2; :: thesis: verum