let D be non empty set ; :: thesis: for A being BinOp of D
for f, g being FinSequence of D
for F1, F2 being finite set
for E1 being Enumeration of F1
for E2 being Enumeration of F2 st card F1 = card F2 & len f <= len g holds
doms ((SignGenOp (f,A,F1)) * E1) c= doms ((SignGenOp (g,A,F2)) * E2)
let A be BinOp of D; :: thesis: for f, g being FinSequence of D
for F1, F2 being finite set
for E1 being Enumeration of F1
for E2 being Enumeration of F2 st card F1 = card F2 & len f <= len g holds
doms ((SignGenOp (f,A,F1)) * E1) c= doms ((SignGenOp (g,A,F2)) * E2)
let f, g be FinSequence of D; :: thesis: for F1, F2 being finite set
for E1 being Enumeration of F1
for E2 being Enumeration of F2 st card F1 = card F2 & len f <= len g holds
doms ((SignGenOp (f,A,F1)) * E1) c= doms ((SignGenOp (g,A,F2)) * E2)
let F1, F2 be finite set ; :: thesis: for E1 being Enumeration of F1
for E2 being Enumeration of F2 st card F1 = card F2 & len f <= len g holds
doms ((SignGenOp (f,A,F1)) * E1) c= doms ((SignGenOp (g,A,F2)) * E2)
let E1 be Enumeration of F1; :: thesis: for E2 being Enumeration of F2 st card F1 = card F2 & len f <= len g holds
doms ((SignGenOp (f,A,F1)) * E1) c= doms ((SignGenOp (g,A,F2)) * E2)
let E2 be Enumeration of F2; :: thesis: ( card F1 = card F2 & len f <= len g implies doms ((SignGenOp (f,A,F1)) * E1) c= doms ((SignGenOp (g,A,F2)) * E2) )
assume A1: ( card F1 = card F2 & len f <= len g ) ; :: thesis: doms ((SignGenOp (f,A,F1)) * E1) c= doms ((SignGenOp (g,A,F2)) * E2)
A2: ( len ((SignGenOp (g,A,F2)) * E2) = len E2 & len E2 = card F2 & len ((SignGenOp (f,A,F1)) * E1) = len E1 & len E1 = card F1 ) by CARD_1:def 7;
A3: dom ((SignGenOp (f,A,F1)) * E1) = dom ((SignGenOp (g,A,F2)) * E2) by A1, A2, FINSEQ_3:29;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in doms ((SignGenOp (f,A,F1)) * E1) or x in doms ((SignGenOp (g,A,F2)) * E2) )
assume A4: x in doms ((SignGenOp (f,A,F1)) * E1) ; :: thesis: x in doms ((SignGenOp (g,A,F2)) * E2)
reconsider x = x as FinSequence by A4;
A5: len x = len ((SignGenOp (g,A,F2)) * E2) by A2, Th47, A4, A1;
for i being Nat st i in dom x holds
x . i in dom (((SignGenOp (g,A,F2)) * E2) . i)

proof

let i be Nat; :: thesis: ( i in dom x implies x . i in dom (((SignGenOp (g,A,F2)) * E2) . i) )
assume A6: i in dom x ; :: thesis: x . i in dom (((SignGenOp (g,A,F2)) * E2) . i)
A7: x . i in dom (((SignGenOp (f,A,F1)) * E1) . i) by A6, A4, Th47;
((SignGenOp (f,A,F1)) * E1) . i <> {} by A6, A4, Th47;
then i in dom ((SignGenOp (f,A,F1)) * E1) by FUNCT_1:def 2;
then ( ((SignGenOp (g,A,F2)) * E2) . i = SignGen (g,A,(E2 . i)) & ((SignGenOp (f,A,F1)) * E1) . i = SignGen (f,A,(E1 . i)) ) by A3, Th80;
then ( len (((SignGenOp (g,A,F2)) * E2) . i) = len g & len (((SignGenOp (f,A,F1)) * E1) . i) = len f ) by CARD_1:def 7;
then dom (((SignGenOp (f,A,F1)) * E1) . i) c= dom (((SignGenOp (g,A,F2)) * E2) . i) by A1, FINSEQ_3:30;
hence x . i in dom (((SignGenOp (g,A,F2)) * E2) . i) by A7; :: thesis: verum

end;

hence x in doms ((SignGenOp (g,A,F2)) * E2) by A5, Th47; :: thesis: verum