let D be non empty set ; :: thesis: for A being BinOp of D
for f 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 holds
doms ((SignGenOp (f,A,F1)) * E1) = doms ((SignGenOp (f,A,F2)) * E2)
let A be BinOp of D; :: thesis: for f 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 holds
doms ((SignGenOp (f,A,F1)) * E1) = doms ((SignGenOp (f,A,F2)) * E2)
let f 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 holds
doms ((SignGenOp (f,A,F1)) * E1) = doms ((SignGenOp (f,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 holds
doms ((SignGenOp (f,A,F1)) * E1) = doms ((SignGenOp (f,A,F2)) * E2)
let E1 be Enumeration of F1; :: thesis: for E2 being Enumeration of F2 st card F1 = card F2 holds
doms ((SignGenOp (f,A,F1)) * E1) = doms ((SignGenOp (f,A,F2)) * E2)
let E2 be Enumeration of F2; :: thesis: ( card F1 = card F2 implies doms ((SignGenOp (f,A,F1)) * E1) = doms ((SignGenOp (f,A,F2)) * E2) )
assume A1: card F1 = card F2 ; :: thesis: doms ((SignGenOp (f,A,F1)) * E1) = doms ((SignGenOp (f,A,F2)) * E2)
A2: ( len ((SignGenOp (f,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 (f,A,F2)) * E2) by A1, A2, FINSEQ_3:29;
thus doms ((SignGenOp (f,A,F1)) * E1) c= doms ((SignGenOp (f,A,F2)) * E2) :: according to XBOOLE_0:def 10 :: thesis: doms ((SignGenOp (f,A,F2)) * E2) c= doms ((SignGenOp (f,A,F1)) * E1)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in doms ((SignGenOp (f,A,F1)) * E1) or x in doms ((SignGenOp (f,A,F2)) * E2) )
assume A4: x in doms ((SignGenOp (f,A,F1)) * E1) ; :: thesis: x in doms ((SignGenOp (f,A,F2)) * E2)
reconsider x = x as FinSequence by A4;
A5: len x = len ((SignGenOp (f,A,F2)) * E2) by A2, Th47, A4, A1;
for i being Nat st i in dom x holds
x . i in dom (((SignGenOp (f,A,F2)) * E2) . i)

proof

let i be Nat; :: thesis: ( i in dom x implies x . i in dom (((SignGenOp (f,A,F2)) * E2) . i) )
assume A6: i in dom x ; :: thesis: x . i in dom (((SignGenOp (f,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 (f,A,F2)) * E2) . i = SignGen (f,A,(E2 . i)) & ((SignGenOp (f,A,F1)) * E1) . i = SignGen (f,A,(E1 . i)) ) by A3, Th80;
then ( len (((SignGenOp (f,A,F2)) * E2) . i) = len f & len (((SignGenOp (f,A,F1)) * E1) . i) = len f ) by CARD_1:def 7;
hence x . i in dom (((SignGenOp (f,A,F2)) * E2) . i) by A7, FINSEQ_3:29; :: thesis: verum

end;

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

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in doms ((SignGenOp (f,A,F2)) * E2) or x in doms ((SignGenOp (f,A,F1)) * E1) )
assume A8: x in doms ((SignGenOp (f,A,F2)) * E2) ; :: thesis: x in doms ((SignGenOp (f,A,F1)) * E1)
reconsider x = x as FinSequence by A8;
A9: len x = len ((SignGenOp (f,A,F1)) * E1) by A2, Th47, A8, A1;
for i being Nat st i in dom x holds
x . i in dom (((SignGenOp (f,A,F1)) * E1) . i)

proof

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

end;

hence x in doms ((SignGenOp (f,A,F1)) * E1) by A9, Th47; :: thesis: verum