let D be non empty set ; :: thesis: for A being BinOp of D
for f, g being FinSequence of D
for F1 being finite set
for E1 being Enumeration of F1 holds doms ((SignGenOp (f,A,F1)) * E1) c= doms ((SignGenOp ((f ^ g),A,F1)) * E1)
let A be BinOp of D; :: thesis: for f, g being FinSequence of D
for F1 being finite set
for E1 being Enumeration of F1 holds doms ((SignGenOp (f,A,F1)) * E1) c= doms ((SignGenOp ((f ^ g),A,F1)) * E1)
let f, g be FinSequence of D; :: thesis: for F1 being finite set
for E1 being Enumeration of F1 holds doms ((SignGenOp (f,A,F1)) * E1) c= doms ((SignGenOp ((f ^ g),A,F1)) * E1)
let F1 be finite set ; :: thesis: for E1 being Enumeration of F1 holds doms ((SignGenOp (f,A,F1)) * E1) c= doms ((SignGenOp ((f ^ g),A,F1)) * E1)
let E1 be Enumeration of F1; :: thesis: doms ((SignGenOp (f,A,F1)) * E1) c= doms ((SignGenOp ((f ^ g),A,F1)) * E1)
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 ^ g),A,F1)) * E1) )
assume A1: x in doms ((SignGenOp (f,A,F1)) * E1) ; :: thesis: x in doms ((SignGenOp ((f ^ g),A,F1)) * E1)
reconsider x = x as FinSequence by A1;
A2: len ((SignGenOp (f,A,F1)) * E1) = len E1 by CARD_1:def 7;
then A3: len x = len E1 by A1, Th47;
then A4: len x = len ((SignGenOp ((f ^ g),A,F1)) * E1) by CARD_1:def 7;
then A5: dom x = dom ((SignGenOp ((f ^ g),A,F1)) * E1) by FINSEQ_3:30;
A6: dom x = dom ((SignGenOp (f,A,F1)) * E1) by A2, A3, FINSEQ_3:30;
for i being Nat st i in dom x holds
x . i in dom (((SignGenOp ((f ^ g),A,F1)) * E1) . i)

proof

let i be Nat; :: thesis: ( i in dom x implies x . i in dom (((SignGenOp ((f ^ g),A,F1)) * E1) . i) )
assume A7: i in dom x ; :: thesis: x . i in dom (((SignGenOp ((f ^ g),A,F1)) * E1) . i)
A8: dom f c= dom (f ^ g) by FINSEQ_1:26;
A9: x . i in dom (((SignGenOp (f,A,F1)) * E1) . i) by A7, A1, Th47;
((SignGenOp (f,A,F1)) * E1) . i = SignGen (f,A,(E1 . i)) by Th80, A7, A6;
then len (((SignGenOp (f,A,F1)) * E1) . i) = len f by CARD_1:def 7;
then A10: dom (((SignGenOp (f,A,F1)) * E1) . i) = dom f by FINSEQ_3:30;
((SignGenOp ((f ^ g),A,F1)) * E1) . i = SignGen ((f ^ g),A,(E1 . i)) by A7, A5, Th80;
then len (((SignGenOp ((f ^ g),A,F1)) * E1) . i) = len (f ^ g) by CARD_1:def 7;
then dom (((SignGenOp ((f ^ g),A,F1)) * E1) . i) = dom (f ^ g) by FINSEQ_3:30;
hence x . i in dom (((SignGenOp ((f ^ g),A,F1)) * E1) . i) by A8, A9, A10; :: thesis: verum

end;

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