let I be set ; :: thesis: for A, B being ManySortedSet of I st A c= B holds
product A c= product B
let A, B be ManySortedSet of I; :: thesis: ( A c= B implies product A c= product B )
assume A1: A c= B ; :: thesis: product A c= product B
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in product A or x in product B )
assume x in product A ; :: thesis: x in product B
then consider g being Function such that
A2: ( x = g & dom g = dom A & ( for y being object st y in dom A holds
g . y in A . y ) ) by CARD_3:def 5;
A3: ( dom A = I & dom B = I ) by PARTFUN1:def 2;
now :: thesis: for y being object st y in I holds
g . y in B . y
let y be object ; :: thesis: ( y in I implies g . y in B . y )
assume y in I ; :: thesis: g . y in B . y
then ( g . y in A . y & A . y c= B . y ) by A1, A2, A3;
hence g . y in B . y ; :: thesis: verum
end;
hence x in product B by A2, A3, CARD_3:9; :: thesis: verum