let X be set ; :: thesis: for P, Q being a_partition of X
for f being Function of P,Q st ( for a being set st a in P holds
a c= f . a ) holds
for p being FinSequence of P
for q being FinSequence of Q holds
( product p c= product q iff f * p = q )
let P, Q be a_partition of X; :: thesis: for f being Function of P,Q st ( for a being set st a in P holds
a c= f . a ) holds
for p being FinSequence of P
for q being FinSequence of Q holds
( product p c= product q iff f * p = q )
let f be Function of P,Q; :: thesis: ( ( for a being set st a in P holds
a c= f . a ) implies for p being FinSequence of P
for q being FinSequence of Q holds
( product p c= product q iff f * p = q ) )
assume A1: for a being set st a in P holds
a c= f . a ; :: thesis: for p being FinSequence of P
for q being FinSequence of Q holds
( product p c= product q iff f * p = q )
let p be FinSequence of P; :: thesis: for q being FinSequence of Q holds
( product p c= product q iff f * p = q )
let q be FinSequence of Q; :: thesis: ( product p c= product q iff f * p = q )
A2: ( rng p c= P & rng q c= Q ) ;

now

assume P <> {} ; :: thesis: Q <> {}
then reconsider X = X as non empty set by EQREL_1:41;
Q is a_partition of X ;
hence Q <> {} ; :: thesis: verum

end;

then ( dom f = P & rng f c= Q ) by FUNCT_2:def 1;
then A3: dom (f * p) = dom p by A2, RELAT_1:46;

hereby :: thesis: ( f * p = q implies product p c= product q )

assume product p c= product q ; :: thesis: f * p = q
then A4: ( dom p = dom q & ( for x being set st x in dom p holds
p . x c= q . x ) ) by Th1;

now

let x be set ; :: thesis: ( x in dom p implies (f * p) . x = q . x )
assume A5: x in dom p ; :: thesis: (f * p) . x = q . x
then A6: ( p . x c= q . x & p . x in rng p & q . x in rng q ) by A4, FUNCT_1:def 5;
then reconsider Y = X as non empty set by EQREL_1:41;
reconsider P' = P, Q' = Q as a_partition of Y ;
reconsider a = p . x as Element of P' by A6;
consider z being Element of a;
( a c= f . a & z in a & f is Function of P',Q' ) by A1;
then ( z in f . a & z in q . x & f . a in Q' ) by A6, FUNCT_2:7;
then q . x = f . a by A6, Th3;
hence (f * p) . x = q . x by A5, FUNCT_1:23; :: thesis: verum

end;

hence f * p = q by A3, A4, FUNCT_1:9; :: thesis: verum

end;

assume A7: f * p = q ; :: thesis: product p c= product q

now

let x be set ; :: thesis: ( x in dom p implies p . x c= q . x )
assume x in dom p ; :: thesis: p . x c= q . x
then ( q . x = f . (p . x) & p . x in rng p ) by A7, FUNCT_1:23, FUNCT_1:def 5;
hence p . x c= q . x by A1; :: thesis: verum

end;

hence product p c= product q by A3, A7, CARD_3:38; :: thesis: verum