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 ;

now :: thesis: ( P <> {} implies Q <> {} )

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

end;

then dom f = P by FUNCT_2:def 1;
then A3: dom (f * p) = dom p by A2, RELAT_1:27;

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

assume A4: product p c= product q ; :: thesis: f * p = q
then A5: dom p = dom q by Th1;

now :: thesis: for x being object st x in dom p holds
(f * p) . x = q . x

let x be object ; :: thesis: ( x in dom p implies (f * p) . x = q . x )
assume A6: x in dom p ; :: thesis: (f * p) . x = q . x
then A7: p . x c= q . x by A4, Th1;
A8: p . x in rng p by A6, FUNCT_1:def 3;
A9: q . x in rng q by A5, A6, FUNCT_1:def 3;
reconsider Y = X as non empty set by A8;
reconsider P9 = P, Q9 = Q as a_partition of Y ;
reconsider a = p . x as Element of P9 by A8;
set z = the Element of a;
A10: a c= f . a by A1;
A11: the Element of a in a ;
f . a in Q9 by FUNCT_2:5;
then q . x = f . a by A7, A9, A10, A11, Lm3;
hence (f * p) . x = q . x by A6, FUNCT_1:13; :: thesis: verum

end;

hence f * p = q by A3, A5; :: thesis: verum

end;

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

now :: thesis: for x being object st x in dom p holds
p . x c= q . x

let x be object ; :: thesis: ( x in dom p implies p . x c= q . x )
assume A13: x in dom p ; :: thesis: p . x c= q . x
then A14: q . x = f . (p . x) by A12, FUNCT_1:13;
p . x in rng p by A13, FUNCT_1:def 3;
hence p . x c= q . x by A1, A14; :: thesis: verum

end;

hence product p c= product q by A3, A12, CARD_3:27; :: thesis: verum