let p be RelStr-yielding ManySortedSet of {0}; :: thesis: for z being Element of {0} holds p . z, product p are_isomorphic

let z be Element of {0}; :: thesis: p . z, product p are_isomorphic

deffunc H_{1}( 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 = H_{1}(x)
from FUNCT_1:sch 3();

A3: z = 0 by TARSKI:def 1;

A4: 0 in {0} by TARSKI:def 1;

let z be Element of {0}; :: thesis: p . z, product p are_isomorphic

deffunc H

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 = H

A3: z = 0 by TARSKI:def 1;

A4: 0 in {0} 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 (product p)

then reconsider f = f as Function of (p . z),(product p) by A1, FUNCT_2:3;f . x in the carrier of (product p)

let x be object ; :: thesis: ( x in the carrier of (p . z) implies f . x in the carrier of (product p) )

assume A5: x in the carrier of (p . z) ; :: thesis: f . x in the carrier of (product p)

then A6: f . x = 0 .--> x by A2;

set g = 0 .--> x;

A7: dom (0 .--> x) = {0}

.= dom (Carrier p) by PARTFUN1:def 2 ;

hence f . x in the carrier of (product p) by YELLOW_1:def 4; :: thesis: verum

end;assume A5: x in the carrier of (p . z) ; :: thesis: f . x in the carrier of (product p)

then A6: f . x = 0 .--> x by A2;

set g = 0 .--> x;

A7: dom (0 .--> x) = {0}

.= dom (Carrier p) by PARTFUN1:def 2 ;

now :: thesis: for y being object st y in dom (Carrier p) holds

(0 .--> x) . y in (Carrier p) . y

then
f . x in product (Carrier p)
by A6, A7, CARD_3:def 5;(0 .--> x) . y in (Carrier p) . y

let y be object ; :: thesis: ( y in dom (Carrier p) implies (0 .--> x) . y in (Carrier p) . y )

assume y in dom (Carrier p) ; :: thesis: (0 .--> x) . y in (Carrier p) . y

then A8: y in {0} ;

then A9: y = 0 by TARSKI:def 1;

ex R being 1-sorted st

( R = p . y & (Carrier p) . y = the carrier of R ) by A8, PRALG_1:def 15;

hence (0 .--> x) . y in (Carrier p) . y by A3, A5, A9; :: thesis: verum

end;assume y in dom (Carrier p) ; :: thesis: (0 .--> x) . y in (Carrier p) . y

then A8: y in {0} ;

then A9: y = 0 by TARSKI:def 1;

ex R being 1-sorted st

( R = p . y & (Carrier p) . y = the carrier of R ) by A8, PRALG_1:def 15;

hence (0 .--> x) . y in (Carrier p) . y by A3, A5, A9; :: thesis: verum

hence f . x in the carrier of (product p) by YELLOW_1:def 4; :: thesis: verum

now :: thesis: f is isomorphic end;

hence
p . z, product p are_isomorphic
by WAYBEL_1:def 8; :: thesis: verumper cases
( p . z is empty or not p . z is empty )
;

end;

suppose A10:
p . z is empty
; :: thesis: f is isomorphic

hence f is isomorphic by A10, WAYBEL_0:def 38; :: thesis: verum

end;

now :: thesis: the carrier of (product p) is empty

then
product p is empty
;assume
not the carrier of (product p) is empty
; :: thesis: contradiction

then A11: not product (Carrier p) is empty by YELLOW_1:def 4;

set x = the Element of product (Carrier p);

A12: ex g being Function st

( the Element of product (Carrier p) = g & dom g = dom (Carrier p) & ( for y being object st y in dom (Carrier p) holds

g . y in (Carrier p) . y ) ) by A11, CARD_3:def 5;

A13: 0 in dom (Carrier p) by A4, PARTFUN1:def 2;

consider R being 1-sorted such that

A14: R = p . 0 and

A15: (Carrier p) . 0 = the carrier of R by A4, PRALG_1:def 15;

R is empty by A10, A14, TARSKI:def 1;

hence contradiction by A12, A13, A15; :: thesis: verum

end;then A11: not product (Carrier p) is empty by YELLOW_1:def 4;

set x = the Element of product (Carrier p);

A12: ex g being Function st

( the Element of product (Carrier p) = g & dom g = dom (Carrier p) & ( for y being object st y in dom (Carrier p) holds

g . y in (Carrier p) . y ) ) by A11, CARD_3:def 5;

A13: 0 in dom (Carrier p) by A4, PARTFUN1:def 2;

consider R being 1-sorted such that

A14: R = p . 0 and

A15: (Carrier p) . 0 = the carrier of R by A4, PRALG_1:def 15;

R is empty by A10, A14, TARSKI:def 1;

hence contradiction by A12, A13, A15; :: thesis: verum

hence f is isomorphic by A10, WAYBEL_0:def 38; :: thesis: verum

suppose A16:
not p . z is empty
; :: thesis: f is isomorphic

then reconsider pz = p . z as non empty RelStr ;

not product np is empty ;

then reconsider pp = product p as non empty RelStr ;

reconsider f9 = f as Function of pz,pp ;

end;now :: thesis: for i being set st i in rng p holds

i is non empty 1-sorted

then reconsider np = p as RelStr-yielding yielding_non-empty_carriers ManySortedSet of {0} by YELLOW_6:def 2;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 {0} by A17;

then i = p . 0 by A18, TARSKI:def 1;

hence i is non empty 1-sorted by A16, TARSKI:def 1; :: thesis: verum

end;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 {0} by A17;

then i = p . 0 by A18, TARSKI:def 1;

hence i is non empty 1-sorted by A16, TARSKI:def 1; :: thesis: verum

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

then A25:
f is one-to-one
by FUNCT_1:def 4;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 A2, A19

.= [:{0},{x1}:] ;

A23: f . x2 = 0 .--> x2 by A2, A20

.= [:{0},{x2}:] ;

A24: 0 in {0} by TARSKI:def 1;

x1 in {x1} by TARSKI:def 1;

then [0,x1] in f . x2 by A21, A22, A24, ZFMISC_1:def 2;

then ex xa, ya being object st

( xa in {0} & ya in {x2} & [0,x1] = [xa,ya] ) by A23, ZFMISC_1:def 2;

then x1 in {x2} by XTUPLE_0:1;

hence x1 = x2 by TARSKI:def 1; :: thesis: verum

end;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 A2, A19

.= [:{0},{x1}:] ;

A23: f . x2 = 0 .--> x2 by A2, A20

.= [:{0},{x2}:] ;

A24: 0 in {0} by TARSKI:def 1;

x1 in {x1} by TARSKI:def 1;

then [0,x1] in f . x2 by A21, A22, A24, ZFMISC_1:def 2;

then ex xa, ya being object st

( xa in {0} & ya in {x2} & [0,x1] = [xa,ya] ) by A23, ZFMISC_1:def 2;

then x1 in {x2} by XTUPLE_0:1;

hence x1 = x2 by TARSKI:def 1; :: thesis: verum

now :: thesis: for y being object holds

( ( y in rng f implies y in the carrier of (product p) ) & ( y in the carrier of (product p) implies y in rng f ) )

then A34:
rng f = the carrier of (product p)
by TARSKI:2;( ( y in rng f implies y in the carrier of (product p) ) & ( y in the carrier of (product p) implies y in rng f ) )

let y be object ; :: thesis: ( ( y in rng f implies y in the carrier of (product p) ) & ( y in the carrier of (product p) implies y in rng f ) )

thus ( y in rng f implies y in the carrier of (product p) ) ; :: thesis: ( y in the carrier of (product p) implies y in rng f )

assume y in the carrier of (product p) ; :: thesis: y in rng f

then y in product (Carrier p) by YELLOW_1:def 4;

then consider g being Function such that

A26: y = g and

A27: dom g = dom (Carrier p) and

A28: for x being object st x in dom (Carrier p) holds

g . x in (Carrier p) . x by CARD_3:def 5;

A29: dom g = {0} by A27, PARTFUN1:def 2;

A30: 0 in dom (Carrier p) by A4, PARTFUN1:def 2;

A31: ex R being 1-sorted st

( R = p . 0 & (Carrier p) . 0 = the carrier of R ) by A4, PRALG_1:def 15;

A32: g = 0 .--> (g . 0) by A29, Th1;

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 A26, A32, A33, FUNCT_1:def 3; :: thesis: verum

end;thus ( y in rng f implies y in the carrier of (product p) ) ; :: thesis: ( y in the carrier of (product p) implies y in rng f )

assume y in the carrier of (product p) ; :: thesis: y in rng f

then y in product (Carrier p) by YELLOW_1:def 4;

then consider g being Function such that

A26: y = g and

A27: dom g = dom (Carrier p) and

A28: for x being object st x in dom (Carrier p) holds

g . x in (Carrier p) . x by CARD_3:def 5;

A29: dom g = {0} by A27, PARTFUN1:def 2;

A30: 0 in dom (Carrier p) by A4, PARTFUN1:def 2;

A31: ex R being 1-sorted st

( R = p . 0 & (Carrier p) . 0 = the carrier of R ) by A4, PRALG_1:def 15;

A32: g = 0 .--> (g . 0) by A29, Th1;

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 A26, A32, A33, FUNCT_1:def 3; :: thesis: verum

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 ) )

hence
f is isomorphic
by A25, A34, WAYBEL_0:66; :: thesis: verum( ( 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 (Carrier p) is empty by YELLOW_1:def 4;

A36: f9 . x is Element of product (Carrier p) by YELLOW_1:def 4;

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 {0} 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 A35, A36, YELLOW_1:def 4;

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 A4, A42;

f1 = 0 .--> x by A2, A40;

then A47: xi = x by A44, FUNCOP_1:72;

A48: g1 = 0 .--> y by A2, A41;

R = pz by A43, TARSKI:def 1;

hence x <= y by A45, A46, A47, A48, FUNCOP_1:72; :: thesis: verum

end;not product np is empty ;

then A35: not product (Carrier p) is empty by YELLOW_1:def 4;

A36: f9 . x is Element of product (Carrier p) by YELLOW_1:def 4;

hereby :: thesis: ( f9 . x <= f9 . y implies x <= y )

assume
f9 . x <= f9 . y
; :: thesis: x <= yassume 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 {0} holds

ex R being RelStr ex xi, yi being Element of R st

( R = p . i & xi = f1 . i & yi = g1 . i & xi <= yi ) ) )

end;ex f1, g1 being Function st

( f1 = f9 . x & g1 = f9 . y & ( for i being object st i in {0} 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

hence
f9 . x <= f9 . y
by A35, A36, YELLOW_1:def 4; :: thesis: verum
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 {0} 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 {0} 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 {0} 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 {0} 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 {0} 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 {0} ; :: 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 A38, TARSKI:def 1;

0 in dom p by A4, PARTFUN1:def 2;

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 A38, TARSKI:def 1; :: thesis: ( x9 = f1 . i & y9 = g1 . i & x9 <= y9 )

thus x9 = f1 . i by A39, FUNCOP_1:72; :: thesis: ( y9 = g1 . i & x9 <= y9 )

thus y9 = g1 . i by A39, FUNCOP_1:72; :: thesis: x9 <= y9

thus x9 <= y9 by A37, TARSKI:def 1; :: thesis: verum

end;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 {0} 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 {0} 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 {0} 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 {0} 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 {0} 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 {0} ; :: 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 A38, TARSKI:def 1;

0 in dom p by A4, PARTFUN1:def 2;

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 A38, TARSKI:def 1; :: thesis: ( x9 = f1 . i & y9 = g1 . i & x9 <= y9 )

thus x9 = f1 . i by A39, FUNCOP_1:72; :: thesis: ( y9 = g1 . i & x9 <= y9 )

thus y9 = g1 . i by A39, FUNCOP_1:72; :: thesis: x9 <= y9

thus x9 <= y9 by A37, TARSKI:def 1; :: thesis: verum

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 {0} 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 A35, A36, YELLOW_1:def 4;

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 A4, A42;

f1 = 0 .--> x by A2, A40;

then A47: xi = x by A44, FUNCOP_1:72;

A48: g1 = 0 .--> y by A2, A41;

R = pz by A43, TARSKI:def 1;

hence x <= y by A45, A46, A47, A48, FUNCOP_1:72; :: thesis: verum