let a, b, c be object ; :: thesis: for A, B, C, D, E, F being set st A c= B & C c= D & E c= F holds
product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F))
let A, B, C, D, E, F be set ; :: thesis: ( A c= B & C c= D & E c= F implies product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F)) )
assume A1: ( A c= B & C c= D & E c= F ) ; :: thesis: product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F))
set f = (a,b,c) --> (A,C,E);
set g = (a,b,c) --> (B,D,F);
A2: ( dom ((a,b,c) --> (A,C,E)) = {a,b,c} & dom ((a,b,c) --> (B,D,F)) = {a,b,c} ) by FUNCT_4:128;
per cases ( ( a = c & a <> b ) or ( b = c & a <> b ) or a = b or ( a <> b & a <> c & b <> c ) ) ;
suppose ( a = c & a <> b ) ; :: thesis: product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F))
then ( (a,b,c) --> (A,C,E) = (a,b) --> (E,C) & (a,b,c) --> (B,D,F) = (a,b) --> (F,D) ) by FUNCT_4:132;
hence product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F)) by A1, TOPREAL6:21; :: thesis: verum
end;
suppose ( b = c & a <> b ) ; :: thesis: product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F))
then ( (a,b,c) --> (A,C,E) = (a,b) --> (A,E) & (a,b,c) --> (B,D,F) = (a,b) --> (B,F) ) by FUNCT_4:133;
hence product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F)) by A1, TOPREAL6:21; :: thesis: verum
end;
suppose a = b ; :: thesis: product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F))
then ( (a,b,c) --> (A,C,E) = (a,c) --> (C,E) & (a,b,c) --> (B,D,F) = (a,c) --> (D,F) ) by FUNCT_4:81;
hence product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F)) by A1, TOPREAL6:21; :: thesis: verum
end;
suppose A3: ( a <> b & a <> c & b <> c ) ; :: thesis: product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F))
for x being object st x in dom ((a,b,c) --> (A,C,E)) holds
((a,b,c) --> (A,C,E)) . x c= ((a,b,c) --> (B,D,F)) . x
proof
let x be object ; :: thesis: ( x in dom ((a,b,c) --> (A,C,E)) implies ((a,b,c) --> (A,C,E)) . x c= ((a,b,c) --> (B,D,F)) . x )
assume x in dom ((a,b,c) --> (A,C,E)) ; :: thesis: ((a,b,c) --> (A,C,E)) . x c= ((a,b,c) --> (B,D,F)) . x
then A4: ( x = a or x = b or x = c ) by A2, ENUMSET1:def 1;
a,b,c are_mutually_distinct by A3;
then ( ((a,b,c) --> (A,C,E)) . a = A & ((a,b,c) --> (A,C,E)) . b = C & ((a,b,c) --> (A,C,E)) . c = E & ((a,b,c) --> (B,D,F)) . a = B & ((a,b,c) --> (B,D,F)) . b = D & ((a,b,c) --> (B,D,F)) . c = F ) by FUNCT_4:135, FUNCT_4:134;
hence ((a,b,c) --> (A,C,E)) . x c= ((a,b,c) --> (B,D,F)) . x by A1, A4; :: thesis: verum
end;
hence product ((a,b,c) --> (A,C,E)) c= product ((a,b,c) --> (B,D,F)) by A2, CARD_3:27; :: thesis: verum
end;
end;