let I be non empty finite set ; :: thesis: for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds

for f being Collineation of (Segre_Product A)

for B1, B2 being Segre-Coset of A st B1 misses B2 & B1 '||' B2 holds

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds

canonical_embedding (f,b1) = canonical_embedding (f,b2)

let A be PLS-yielding ManySortedSet of I; :: thesis: ( ( for i being Element of I holds A . i is strongly_connected ) implies for f being Collineation of (Segre_Product A)

for B1, B2 being Segre-Coset of A st B1 misses B2 & B1 '||' B2 holds

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds

canonical_embedding (f,b1) = canonical_embedding (f,b2) )

assume A1: for i being Element of I holds A . i is strongly_connected ; :: thesis: for f being Collineation of (Segre_Product A)

for B1, B2 being Segre-Coset of A st B1 misses B2 & B1 '||' B2 holds

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds

canonical_embedding (f,b1) = canonical_embedding (f,b2)

let f be Collineation of (Segre_Product A); :: thesis: for B1, B2 being Segre-Coset of A st B1 misses B2 & B1 '||' B2 holds

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds

canonical_embedding (f,b1) = canonical_embedding (f,b2)

let B1, B2 be Segre-Coset of A; :: thesis: ( B1 misses B2 & B1 '||' B2 implies for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds

canonical_embedding (f,b1) = canonical_embedding (f,b2) )

assume that

A2: B1 misses B2 and

A3: B1 '||' B2 ; :: thesis: for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds

canonical_embedding (f,b1) = canonical_embedding (f,b2)

let b1, b2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis: ( product b1 = B1 & product b2 = B2 implies canonical_embedding (f,b1) = canonical_embedding (f,b2) )

assume that

A4: product b1 = B1 and

A5: product b2 = B2 ; :: thesis: canonical_embedding (f,b1) = canonical_embedding (f,b2)

A6: indx b1 = indx b2 by A2, A3, A4, A5, Th21;

reconsider B3 = f .: B1, B4 = f .: B2 as Segre-Coset of A by A1, PENCIL_2:24;

A7: f is bijective by PENCIL_2:def 4;

then A8: B3 misses B4 by A2, FUNCT_1:66;

set i = indx b1;

consider r being Element of I such that

A9: r <> indx b1 and

A10: for i being Element of I st i <> r holds

b1 . i = b2 . i and

A11: for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds

c1,c2 are_collinear by A2, A3, A4, A5, Th21;

consider b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that

A12: product b4 = B4 and

A13: b4 . (indx b4) = [#] (A . (indx b4)) by PENCIL_2:def 2;

consider b3 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that

A14: product b3 = B3 and

A15: b3 . (indx b3) = [#] (A . (indx b3)) by PENCIL_2:def 2;

B3 '||' B4 by A3, Th20;

then A16: indx b3 = indx b4 by A8, A14, A12, Th21;

set j = indx b3;

A17: dom f = the carrier of (Segre_Product A) by FUNCT_2:def 1;

A18: dom b1 = I by PARTFUN1:def 2;

hence canonical_embedding (f,b1) = canonical_embedding (f,b2) by A19; :: thesis: verum

for f being Collineation of (Segre_Product A)

for B1, B2 being Segre-Coset of A st B1 misses B2 & B1 '||' B2 holds

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds

canonical_embedding (f,b1) = canonical_embedding (f,b2)

let A be PLS-yielding ManySortedSet of I; :: thesis: ( ( for i being Element of I holds A . i is strongly_connected ) implies for f being Collineation of (Segre_Product A)

for B1, B2 being Segre-Coset of A st B1 misses B2 & B1 '||' B2 holds

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds

canonical_embedding (f,b1) = canonical_embedding (f,b2) )

assume A1: for i being Element of I holds A . i is strongly_connected ; :: thesis: for f being Collineation of (Segre_Product A)

for B1, B2 being Segre-Coset of A st B1 misses B2 & B1 '||' B2 holds

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds

canonical_embedding (f,b1) = canonical_embedding (f,b2)

let f be Collineation of (Segre_Product A); :: thesis: for B1, B2 being Segre-Coset of A st B1 misses B2 & B1 '||' B2 holds

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds

canonical_embedding (f,b1) = canonical_embedding (f,b2)

let B1, B2 be Segre-Coset of A; :: thesis: ( B1 misses B2 & B1 '||' B2 implies for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds

canonical_embedding (f,b1) = canonical_embedding (f,b2) )

assume that

A2: B1 misses B2 and

A3: B1 '||' B2 ; :: thesis: for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 = B1 & product b2 = B2 holds

canonical_embedding (f,b1) = canonical_embedding (f,b2)

let b1, b2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis: ( product b1 = B1 & product b2 = B2 implies canonical_embedding (f,b1) = canonical_embedding (f,b2) )

assume that

A4: product b1 = B1 and

A5: product b2 = B2 ; :: thesis: canonical_embedding (f,b1) = canonical_embedding (f,b2)

A6: indx b1 = indx b2 by A2, A3, A4, A5, Th21;

reconsider B3 = f .: B1, B4 = f .: B2 as Segre-Coset of A by A1, PENCIL_2:24;

A7: f is bijective by PENCIL_2:def 4;

then A8: B3 misses B4 by A2, FUNCT_1:66;

set i = indx b1;

consider r being Element of I such that

A9: r <> indx b1 and

A10: for i being Element of I st i <> r holds

b1 . i = b2 . i and

A11: for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds

c1,c2 are_collinear by A2, A3, A4, A5, Th21;

consider b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that

A12: product b4 = B4 and

A13: b4 . (indx b4) = [#] (A . (indx b4)) by PENCIL_2:def 2;

consider b3 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that

A14: product b3 = B3 and

A15: b3 . (indx b3) = [#] (A . (indx b3)) by PENCIL_2:def 2;

B3 '||' B4 by A3, Th20;

then A16: indx b3 = indx b4 by A8, A14, A12, Th21;

set j = indx b3;

A17: dom f = the carrier of (Segre_Product A) by FUNCT_2:def 1;

A18: dom b1 = I by PARTFUN1:def 2;

A19: now :: thesis: for o being object st o in the carrier of (A . (indx b1)) holds

(canonical_embedding (f,b1)) . o = (canonical_embedding (f,b2)) . o

( dom (canonical_embedding (f,b1)) = the carrier of (A . (indx b1)) & dom (canonical_embedding (f,b2)) = the carrier of (A . (indx b1)) )
by A6, FUNCT_2:def 1;(canonical_embedding (f,b1)) . o = (canonical_embedding (f,b2)) . o

b2 . r is trivial
by A6, A9, PENCIL_1:def 21;

then consider c2 being object such that

A20: b2 . r = {c2} by ZFMISC_1:131;

b2 c= Carrier A by PBOOLE:def 18;

then b2 . r c= (Carrier A) . r ;

then A21: {c2} c= [#] (A . r) by A20, Th7;

let o be object ; :: thesis: ( o in the carrier of (A . (indx b1)) implies (canonical_embedding (f,b1)) . b_{1} = (canonical_embedding (f,b2)) . b_{1} )

consider p0 being object such that

A22: p0 in product b1 by XBOOLE_0:def 1;

assume o in the carrier of (A . (indx b1)) ; :: thesis: (canonical_embedding (f,b1)) . b_{1} = (canonical_embedding (f,b2)) . b_{1}

then reconsider u = o as Point of (A . (indx b1)) ;

reconsider p1 = p0 as Point of (Segre_Product A) by A4, A22;

reconsider p = p1 as ManySortedSet of I by PENCIL_1:14;

set q = p +* ((indx b1),u);

reconsider q1 = p +* ((indx b1),u) as Point of (Segre_Product A) by PENCIL_1:25;

b1 . r is trivial by A9, PENCIL_1:def 21;

then consider c1 being object such that

A23: b1 . r = {c1} by ZFMISC_1:131;

b1 c= Carrier A by PBOOLE:def 18;

then b1 . r c= (Carrier A) . r ;

then {c1} c= [#] (A . r) by A23, Th7;

then reconsider c1 = c1 as Point of (A . r) by ZFMISC_1:31;

reconsider c2 = c2 as Point of (A . r) by A21, ZFMISC_1:31;

set t = (p +* ((indx b1),u)) +* (r,c2);

p +* ((indx b1),u) is Point of (Segre_Product A) by PENCIL_1:25;

then reconsider t1 = (p +* ((indx b1),u)) +* (r,c2) as Point of (Segre_Product A) by PENCIL_1:25;

end;then consider c2 being object such that

A20: b2 . r = {c2} by ZFMISC_1:131;

b2 c= Carrier A by PBOOLE:def 18;

then b2 . r c= (Carrier A) . r ;

then A21: {c2} c= [#] (A . r) by A20, Th7;

let o be object ; :: thesis: ( o in the carrier of (A . (indx b1)) implies (canonical_embedding (f,b1)) . b

consider p0 being object such that

A22: p0 in product b1 by XBOOLE_0:def 1;

assume o in the carrier of (A . (indx b1)) ; :: thesis: (canonical_embedding (f,b1)) . b

then reconsider u = o as Point of (A . (indx b1)) ;

reconsider p1 = p0 as Point of (Segre_Product A) by A4, A22;

reconsider p = p1 as ManySortedSet of I by PENCIL_1:14;

set q = p +* ((indx b1),u);

reconsider q1 = p +* ((indx b1),u) as Point of (Segre_Product A) by PENCIL_1:25;

b1 . r is trivial by A9, PENCIL_1:def 21;

then consider c1 being object such that

A23: b1 . r = {c1} by ZFMISC_1:131;

b1 c= Carrier A by PBOOLE:def 18;

then b1 . r c= (Carrier A) . r ;

then {c1} c= [#] (A . r) by A23, Th7;

then reconsider c1 = c1 as Point of (A . r) by ZFMISC_1:31;

reconsider c2 = c2 as Point of (A . r) by A21, ZFMISC_1:31;

set t = (p +* ((indx b1),u)) +* (r,c2);

p +* ((indx b1),u) is Point of (Segre_Product A) by PENCIL_1:25;

then reconsider t1 = (p +* ((indx b1),u)) +* (r,c2) as Point of (Segre_Product A) by PENCIL_1:25;

per cases
( c1 <> c2 or c1 = c2 )
;

end;

suppose A24:
c1 <> c2
; :: thesis: (canonical_embedding (f,b1)) . b_{1} = (canonical_embedding (f,b2)) . b_{1}

(p +* ((indx b1),u)) . r = p . r
by A9, FUNCT_7:32;

then (p +* ((indx b1),u)) . r in b1 . r by A18, A22, CARD_3:9;

then A25: (p +* ((indx b1),u)) . r = c1 by A23, TARSKI:def 1;

dom (p +* ((indx b1),u)) = I by PARTFUN1:def 2;

then A26: ((p +* ((indx b1),u)) +* (r,c2)) . r = c2 by FUNCT_7:31;

then A28: f . q1,f . t1 are_collinear by Th1;

reconsider fq = f . q1, ft = f . t1 as ManySortedSet of I by PENCIL_1:14;

A29: dom b1 = I by PARTFUN1:def 2;

A30: dom p = I by PARTFUN1:def 2;

then A34: p +* ((indx b1),u) in product b1 by A29, A31, CARD_3:9;

then A39: (p +* ((indx b1),u)) +* (r,c2) in product b2 by A35, CARD_3:9;

then A40: (canonical_embedding (f,b2)) . (((p +* ((indx b1),u)) +* (r,c2)) . (indx b1)) = ft . ((permutation_of_indices f) . (indx b1)) by A1, A5, A6, Def4;

A41: f . q1 <> f . t1 by A17, A7, A24, A25, A26, FUNCT_1:def 4;

dom p = I by PARTFUN1:def 2;

then A51: (p +* ((indx b1),u)) . (indx b1) = o by FUNCT_7:31;

then ((p +* ((indx b1),u)) +* (r,c2)) . (indx b1) = o by A9, FUNCT_7:32;

hence (canonical_embedding (f,b1)) . o = (canonical_embedding (f,b2)) . o by A1, A4, A50, A34, A40, A42, A51, Def4; :: thesis: verum

end;then (p +* ((indx b1),u)) . r in b1 . r by A18, A22, CARD_3:9;

then A25: (p +* ((indx b1),u)) . r = c1 by A23, TARSKI:def 1;

dom (p +* ((indx b1),u)) = I by PARTFUN1:def 2;

then A26: ((p +* ((indx b1),u)) +* (r,c2)) . r = c2 by FUNCT_7:31;

now :: thesis: for q3, t3 being ManySortedSet of I st q3 = q1 & t3 = t1 holds

ex r being Element of I st

( ( for a, b being Point of (A . r) st a = q3 . r & b = t3 . r holds

( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> r holds

q3 . j = t3 . j ) )

then
q1,t1 are_collinear
by A24, A25, A26, Th17;ex r being Element of I st

( ( for a, b being Point of (A . r) st a = q3 . r & b = t3 . r holds

( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> r holds

q3 . j = t3 . j ) )

let q3, t3 be ManySortedSet of I; :: thesis: ( q3 = q1 & t3 = t1 implies ex r being Element of I st

( ( for a, b being Point of (A . r) st a = q3 . r & b = t3 . r holds

( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> r holds

q3 . j = t3 . j ) ) )

assume A27: ( q3 = q1 & t3 = t1 ) ; :: thesis: ex r being Element of I st

( ( for a, b being Point of (A . r) st a = q3 . r & b = t3 . r holds

( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> r holds

q3 . j = t3 . j ) )

take r = r; :: thesis: ( ( for a, b being Point of (A . r) st a = q3 . r & b = t3 . r holds

( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> r holds

q3 . j = t3 . j ) )

thus for a, b being Point of (A . r) st a = q3 . r & b = t3 . r holds

( a <> b & a,b are_collinear ) by A11, A23, A20, A24, A25, A26, A27; :: thesis: for j being Element of I st j <> r holds

q3 . j = t3 . j

let j be Element of I; :: thesis: ( j <> r implies q3 . j = t3 . j )

assume j <> r ; :: thesis: q3 . j = t3 . j

hence q3 . j = t3 . j by A27, FUNCT_7:32; :: thesis: verum

end;( ( for a, b being Point of (A . r) st a = q3 . r & b = t3 . r holds

( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> r holds

q3 . j = t3 . j ) ) )

assume A27: ( q3 = q1 & t3 = t1 ) ; :: thesis: ex r being Element of I st

( ( for a, b being Point of (A . r) st a = q3 . r & b = t3 . r holds

( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> r holds

q3 . j = t3 . j ) )

take r = r; :: thesis: ( ( for a, b being Point of (A . r) st a = q3 . r & b = t3 . r holds

( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> r holds

q3 . j = t3 . j ) )

thus for a, b being Point of (A . r) st a = q3 . r & b = t3 . r holds

( a <> b & a,b are_collinear ) by A11, A23, A20, A24, A25, A26, A27; :: thesis: for j being Element of I st j <> r holds

q3 . j = t3 . j

let j be Element of I; :: thesis: ( j <> r implies q3 . j = t3 . j )

assume j <> r ; :: thesis: q3 . j = t3 . j

hence q3 . j = t3 . j by A27, FUNCT_7:32; :: thesis: verum

then A28: f . q1,f . t1 are_collinear by Th1;

reconsider fq = f . q1, ft = f . t1 as ManySortedSet of I by PENCIL_1:14;

A29: dom b1 = I by PARTFUN1:def 2;

A30: dom p = I by PARTFUN1:def 2;

A31: now :: thesis: for a being object st a in I holds

(p +* ((indx b1),u)) . a in b1 . a

A33:
dom (p +* ((indx b1),u)) = I
by PARTFUN1:def 2;(p +* ((indx b1),u)) . a in b1 . a

let a be object ; :: thesis: ( a in I implies (p +* ((indx b1),u)) . b_{1} in b1 . b_{1} )

assume A32: a in I ; :: thesis: (p +* ((indx b1),u)) . b_{1} in b1 . b_{1}

end;assume A32: a in I ; :: thesis: (p +* ((indx b1),u)) . b

then A34: p +* ((indx b1),u) in product b1 by A29, A31, CARD_3:9;

A35: now :: thesis: for a being object st a in I holds

((p +* ((indx b1),u)) +* (r,c2)) . a in b2 . a

( dom ((p +* ((indx b1),u)) +* (r,c2)) = I & dom b2 = I )
by PARTFUN1:def 2;((p +* ((indx b1),u)) +* (r,c2)) . a in b2 . a

let a be object ; :: thesis: ( a in I implies ((p +* ((indx b1),u)) +* (r,c2)) . b_{1} in b2 . b_{1} )

assume A36: a in I ; :: thesis: ((p +* ((indx b1),u)) +* (r,c2)) . b_{1} in b2 . b_{1}

end;assume A36: a in I ; :: thesis: ((p +* ((indx b1),u)) +* (r,c2)) . b

per cases
( a = r or a <> r )
;

end;

suppose A37:
a = r
; :: thesis: ((p +* ((indx b1),u)) +* (r,c2)) . b_{1} in b2 . b_{1}

then
((p +* ((indx b1),u)) +* (r,c2)) . a = c2
by A33, FUNCT_7:31;

hence ((p +* ((indx b1),u)) +* (r,c2)) . a in b2 . a by A20, A37, TARSKI:def 1; :: thesis: verum

end;hence ((p +* ((indx b1),u)) +* (r,c2)) . a in b2 . a by A20, A37, TARSKI:def 1; :: thesis: verum

suppose A38:
a <> r
; :: thesis: ((p +* ((indx b1),u)) +* (r,c2)) . b_{1} in b2 . b_{1}

then
((p +* ((indx b1),u)) +* (r,c2)) . a = (p +* ((indx b1),u)) . a
by FUNCT_7:32;

then ((p +* ((indx b1),u)) +* (r,c2)) . a in b1 . a by A31, A36;

hence ((p +* ((indx b1),u)) +* (r,c2)) . a in b2 . a by A10, A36, A38; :: thesis: verum

end;then ((p +* ((indx b1),u)) +* (r,c2)) . a in b1 . a by A31, A36;

hence ((p +* ((indx b1),u)) +* (r,c2)) . a in b2 . a by A10, A36, A38; :: thesis: verum

then A39: (p +* ((indx b1),u)) +* (r,c2) in product b2 by A35, CARD_3:9;

then A40: (canonical_embedding (f,b2)) . (((p +* ((indx b1),u)) +* (r,c2)) . (indx b1)) = ft . ((permutation_of_indices f) . (indx b1)) by A1, A5, A6, Def4;

A41: f . q1 <> f . t1 by A17, A7, A24, A25, A26, FUNCT_1:def 4;

A42: now :: thesis: not fq . (indx b3) <> ft . (indx b3)

A50:
indx b3 = (permutation_of_indices f) . (indx b1)
by A1, A4, A14, Def3;consider l being Element of I such that

for a, b being Point of (A . l) st a = fq . l & b = ft . l holds

( a <> b & a,b are_collinear ) and

A43: for j being Element of I st j <> l holds

fq . j = ft . j by A41, A28, Th17;

assume fq . (indx b3) <> ft . (indx b3) ; :: thesis: contradiction

then A44: indx b3 = l by A43;

A45: dom b4 = I by PARTFUN1:def 2;

A46: fq in B3 by A17, A4, A34, FUNCT_1:def 6;

A47: dom b3 = I by PARTFUN1:def 2;

then fq in product b4 by A45, A48, CARD_3:9;

then fq in (product b3) /\ (product b4) by A14, A46, XBOOLE_0:def 4;

hence contradiction by A8, A14, A12; :: thesis: verum

end;for a, b being Point of (A . l) st a = fq . l & b = ft . l holds

( a <> b & a,b are_collinear ) and

A43: for j being Element of I st j <> l holds

fq . j = ft . j by A41, A28, Th17;

assume fq . (indx b3) <> ft . (indx b3) ; :: thesis: contradiction

then A44: indx b3 = l by A43;

A45: dom b4 = I by PARTFUN1:def 2;

A46: fq in B3 by A17, A4, A34, FUNCT_1:def 6;

A47: dom b3 = I by PARTFUN1:def 2;

A48: now :: thesis: for o being object st o in I holds

fq . o in b4 . o

dom fq = I
by PARTFUN1:def 2;fq . o in b4 . o

let o be object ; :: thesis: ( o in I implies fq . b_{1} in b4 . b_{1} )

assume o in I ; :: thesis: fq . b_{1} in b4 . b_{1}

then reconsider o1 = o as Element of I ;

end;assume o in I ; :: thesis: fq . b

then reconsider o1 = o as Element of I ;

then fq in product b4 by A45, A48, CARD_3:9;

then fq in (product b3) /\ (product b4) by A14, A46, XBOOLE_0:def 4;

hence contradiction by A8, A14, A12; :: thesis: verum

dom p = I by PARTFUN1:def 2;

then A51: (p +* ((indx b1),u)) . (indx b1) = o by FUNCT_7:31;

then ((p +* ((indx b1),u)) +* (r,c2)) . (indx b1) = o by A9, FUNCT_7:32;

hence (canonical_embedding (f,b1)) . o = (canonical_embedding (f,b2)) . o by A1, A4, A50, A34, A40, A42, A51, Def4; :: thesis: verum

suppose A52:
c1 = c2
; :: thesis: (canonical_embedding (f,b1)) . b_{1} = (canonical_embedding (f,b2)) . b_{1}

hence (canonical_embedding (f,b1)) . o = (canonical_embedding (f,b2)) . o by A53, FUNCT_1:2; :: thesis: verum

end;

A53: now :: thesis: for o being object st o in I holds

b1 . o = b2 . o

( dom b1 = I & dom b2 = I )
by PARTFUN1:def 2;b1 . o = b2 . o

let o be object ; :: thesis: ( o in I implies b1 . b_{1} = b2 . b_{1} )

assume o in I ; :: thesis: b1 . b_{1} = b2 . b_{1}

then reconsider o1 = o as Element of I ;

end;assume o in I ; :: thesis: b1 . b

then reconsider o1 = o as Element of I ;

hence (canonical_embedding (f,b1)) . o = (canonical_embedding (f,b2)) . o by A53, FUNCT_1:2; :: thesis: verum

hence canonical_embedding (f,b1) = canonical_embedding (f,b2) by A19; :: thesis: verum