let p be RelStr-yielding ManySortedSet of ; :: thesis: for z being Element of holds p . z, product p are_isomorphic
let z be Element of ; :: thesis:
deffunc H1( object ) -> set = 0 .--> \$1;
consider f being Function such that
A1: dom f = the carrier of (p . z) and
A2: for x being object st x in the carrier of (p . z) holds
f . x = H1(x) from A3: z = 0 by TARSKI:def 1;
A4: 0 in by TARSKI:def 1;
now :: thesis: for x being object st x in the carrier of (p . z) holds
f . x in the carrier of ()
let x be object ; :: thesis: ( x in the carrier of (p . z) implies f . x in the carrier of () )
assume A5: x in the carrier of (p . z) ; :: thesis: f . x in the carrier of ()
then A6: f . x = 0 .--> x by A2;
set g = 0 .--> x;
A7: dom () =
.= dom () by PARTFUN1:def 2 ;
now :: thesis: for y being object st y in dom () holds
() . y in () . y
let y be object ; :: thesis: ( y in dom () implies () . y in () . y )
assume y in dom () ; :: thesis: () . y in () . y
then A8: y in ;
then A9: y = 0 by TARSKI:def 1;
ex R being 1-sorted st
( R = p . y & () . y = the carrier of R ) by ;
hence (0 .--> x) . y in () . y by A3, A5, A9; :: thesis: verum
end;
then f . x in product () by ;
hence f . x in the carrier of () by YELLOW_1:def 4; :: thesis: verum
end;
then reconsider f = f as Function of (p . z),() by ;
now :: thesis: f is isomorphic
per cases ( p . z is empty or not p . z is empty ) ;
suppose A10: p . z is empty ; :: thesis: f is isomorphic
now :: thesis: the carrier of () is empty
assume not the carrier of () is empty ; :: thesis: contradiction
then A11: not product () is empty by YELLOW_1:def 4;
set x = the Element of product ();
A12: ex g being Function st
( the Element of product () = g & dom g = dom () & ( for y being object st y in dom () holds
g . y in () . y ) ) by ;
A13: 0 in dom () by ;
consider R being 1-sorted such that
A14: R = p . 0 and
A15: (Carrier p) . 0 = the carrier of R by ;
R is empty by ;
hence contradiction by A12, A13, A15; :: thesis: verum
end;
then product p is empty ;
hence f is isomorphic by ; :: thesis: verum
end;
suppose A16: not p . z is empty ; :: thesis: f is isomorphic
then reconsider pz = p . z as non empty RelStr ;
now :: thesis: for i being set st i in rng p holds
i is non empty 1-sorted
let i be set ; :: thesis: ( i in rng p implies i is non empty 1-sorted )
assume i in rng p ; :: thesis: i is non empty 1-sorted
then consider x being object such that
A17: x in dom p and
A18: i = p . x by FUNCT_1:def 3;
x in by A17;
then i = p . 0 by ;
hence i is non empty 1-sorted by ; :: thesis: verum
end;
then reconsider np = p as RelStr-yielding yielding_non-empty_carriers ManySortedSet of by YELLOW_6:def 2;
not product np is empty ;
then reconsider pp = product p as non empty RelStr ;
now :: thesis: for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A19: x1 in dom f and
A20: x2 in dom f and
A21: f . x1 = f . x2 ; :: thesis: x1 = x2
A22: f . x1 = 0 .--> x1 by
.= [:,{x1}:] ;
A23: f . x2 = 0 .--> x2 by
.= [:,{x2}:] ;
A24: 0 in by TARSKI:def 1;
x1 in {x1} by TARSKI:def 1;
then [0,x1] in f . x2 by ;
then ex xa, ya being object st
( xa in & ya in {x2} & [0,x1] = [xa,ya] ) by ;
then x1 in {x2} by XTUPLE_0:1;
hence x1 = x2 by TARSKI:def 1; :: thesis: verum
end;
then A25: f is one-to-one by FUNCT_1:def 4;
now :: thesis: for y being object holds
( ( y in rng f implies y in the carrier of () ) & ( y in the carrier of () implies y in rng f ) )
let y be object ; :: thesis: ( ( y in rng f implies y in the carrier of () ) & ( y in the carrier of () implies y in rng f ) )
thus ( y in rng f implies y in the carrier of () ) ; :: thesis: ( y in the carrier of () implies y in rng f )
assume y in the carrier of () ; :: thesis: y in rng f
then y in product () by YELLOW_1:def 4;
then consider g being Function such that
A26: y = g and
A27: dom g = dom () and
A28: for x being object st x in dom () holds
g . x in () . x by CARD_3:def 5;
A29: dom g = by ;
A30: 0 in dom () by ;
A31: ex R being 1-sorted st
( R = p . 0 & () . 0 = the carrier of R ) by ;
A32: g = 0 .--> (g . 0) by ;
A33: f . (g . 0) = 0 .--> (g . 0) by A2, A3, A28, A30, A31;
g . 0 in dom f by A1, A3, A28, A30, A31;
hence y in rng f by ; :: thesis: verum
end;
then A34: rng f = the carrier of () by TARSKI:2;
reconsider f9 = f as Function of pz,pp ;
now :: thesis: for x, y being Element of pz holds
( ( x <= y implies f9 . x <= f9 . y ) & ( f9 . x <= f9 . y implies x <= y ) )
let x, y be Element of pz; :: thesis: ( ( x <= y implies f9 . x <= f9 . y ) & ( f9 . x <= f9 . y implies x <= y ) )
not product np is empty ;
then A35: not product () is empty by YELLOW_1:def 4;
A36: f9 . x is Element of product () by YELLOW_1:def 4;
hereby :: thesis: ( f9 . x <= f9 . y implies x <= y )
assume A37: x <= y ; :: thesis: f9 . x <= f9 . y
ex f1, g1 being Function st
( f1 = f9 . x & g1 = f9 . y & ( for i being object st i in holds
ex R being RelStr ex xi, yi being Element of R st
( R = p . i & xi = f1 . i & yi = g1 . i & xi <= yi ) ) )
proof
set f1 = 0 .--> x;
set g1 = 0 .--> y;
reconsider f1 = 0 .--> x as Function ;
reconsider g1 = 0 .--> y as Function ;
take f1 ; :: thesis: ex g1 being Function st
( f1 = f9 . x & g1 = f9 . y & ( for i being object st i in holds
ex R being RelStr ex xi, yi being Element of R st
( R = p . i & xi = f1 . i & yi = g1 . i & xi <= yi ) ) )

take g1 ; :: thesis: ( f1 = f9 . x & g1 = f9 . y & ( for i being object st i in holds
ex R being RelStr ex xi, yi being Element of R st
( R = p . i & xi = f1 . i & yi = g1 . i & xi <= yi ) ) )

thus f1 = f9 . x by A2; :: thesis: ( g1 = f9 . y & ( for i being object st i in holds
ex R being RelStr ex xi, yi being Element of R st
( R = p . i & xi = f1 . i & yi = g1 . i & xi <= yi ) ) )

thus g1 = f9 . y by A2; :: thesis: for i being object st i in holds
ex R being RelStr ex xi, yi being Element of R st
( R = p . i & xi = f1 . i & yi = g1 . i & xi <= yi )

let i be object ; :: thesis: ( i in implies ex R being RelStr ex xi, yi being Element of R st
( R = p . i & xi = f1 . i & yi = g1 . i & xi <= yi ) )

assume A38: i in ; :: thesis: ex R being RelStr ex xi, yi being Element of R st
( R = p . i & xi = f1 . i & yi = g1 . i & xi <= yi )

A39: i = 0 by ;
0 in dom p by ;
then p . 0 in rng p by FUNCT_1:def 3;
then reconsider p0 = p . 0 as RelStr by YELLOW_1:def 3;
set R = p0;
reconsider x9 = x as Element of p0 by TARSKI:def 1;
reconsider y9 = y as Element of p0 by TARSKI:def 1;
take p0 ; :: thesis: ex xi, yi being Element of p0 st
( p0 = p . i & xi = f1 . i & yi = g1 . i & xi <= yi )

take x9 ; :: thesis: ex yi being Element of p0 st
( p0 = p . i & x9 = f1 . i & yi = g1 . i & x9 <= yi )

take y9 ; :: thesis: ( p0 = p . i & x9 = f1 . i & y9 = g1 . i & x9 <= y9 )
thus p0 = p . i by ; :: thesis: ( x9 = f1 . i & y9 = g1 . i & x9 <= y9 )
thus x9 = f1 . i by ; :: thesis: ( y9 = g1 . i & x9 <= y9 )
thus y9 = g1 . i by ; :: thesis: x9 <= y9
thus x9 <= y9 by ; :: thesis: verum
end;
hence f9 . x <= f9 . y by ; :: thesis: verum
end;
assume f9 . x <= f9 . y ; :: thesis: x <= y
then consider f1, g1 being Function such that
A40: f1 = f9 . x and
A41: g1 = f9 . y and
A42: for i being object st i in holds
ex R being RelStr ex xi, yi being Element of R st
( R = p . i & xi = f1 . i & yi = g1 . i & xi <= yi ) by ;
consider R being RelStr , xi, yi being Element of R such that
A43: R = p . 0 and
A44: xi = f1 . 0 and
A45: yi = g1 . 0 and
A46: xi <= yi by ;
f1 = 0 .--> x by ;
then A47: xi = x by ;
A48: g1 = 0 .--> y by ;
R = pz by ;
hence x <= y by ; :: thesis: verum
end;
hence f is isomorphic by ; :: thesis: verum
end;
end;
end;
hence p . z, product p are_isomorphic by WAYBEL_1:def 8; :: thesis: verum