let f be trivial Function; :: thesis: for x being object st x in dom f holds

proj (f,x) is one-to-one

let x be object ; :: thesis: ( x in dom f implies proj (f,x) is one-to-one )

assume A1: x in dom f ; :: thesis: proj (f,x) is one-to-one

then consider t being object such that

A2: dom f = {t} by ZFMISC_1:131;

A3: dom f = {x} by A1, A2, TARSKI:def 1;

set F = proj (f,x);

for y, z being object st y in dom (proj (f,x)) & z in dom (proj (f,x)) & (proj (f,x)) . y = (proj (f,x)) . z holds

y = z

proj (f,x) is one-to-one

let x be object ; :: thesis: ( x in dom f implies proj (f,x) is one-to-one )

assume A1: x in dom f ; :: thesis: proj (f,x) is one-to-one

then consider t being object such that

A2: dom f = {t} by ZFMISC_1:131;

A3: dom f = {x} by A1, A2, TARSKI:def 1;

set F = proj (f,x);

for y, z being object st y in dom (proj (f,x)) & z in dom (proj (f,x)) & (proj (f,x)) . y = (proj (f,x)) . z holds

y = z

proof

hence
proj (f,x) is one-to-one
by FUNCT_1:def 4; :: thesis: verum
let y, z be object ; :: thesis: ( y in dom (proj (f,x)) & z in dom (proj (f,x)) & (proj (f,x)) . y = (proj (f,x)) . z implies y = z )

assume A4: ( y in dom (proj (f,x)) & z in dom (proj (f,x)) & (proj (f,x)) . y = (proj (f,x)) . z ) ; :: thesis: y = z

then consider g being Function such that

A5: ( y = g & dom g = dom f ) and

for s being object st s in dom f holds

g . s in f . s by CARD_3:def 5;

consider h being Function such that

A6: ( z = h & dom h = dom f ) and

for s being object st s in dom f holds

h . s in f . s by A4, CARD_3:def 5;

A7: g . x = (proj (f,x)) . z by A4, A5, CARD_3:def 16

.= h . x by A4, A6, CARD_3:def 16 ;

for s being object st s in dom g holds

g . s = h . s

end;assume A4: ( y in dom (proj (f,x)) & z in dom (proj (f,x)) & (proj (f,x)) . y = (proj (f,x)) . z ) ; :: thesis: y = z

then consider g being Function such that

A5: ( y = g & dom g = dom f ) and

for s being object st s in dom f holds

g . s in f . s by CARD_3:def 5;

consider h being Function such that

A6: ( z = h & dom h = dom f ) and

for s being object st s in dom f holds

h . s in f . s by A4, CARD_3:def 5;

A7: g . x = (proj (f,x)) . z by A4, A5, CARD_3:def 16

.= h . x by A4, A6, CARD_3:def 16 ;

for s being object st s in dom g holds

g . s = h . s

proof

hence
y = z
by A5, A6, FUNCT_1:2; :: thesis: verum
let s be object ; :: thesis: ( s in dom g implies g . s = h . s )

assume s in dom g ; :: thesis: g . s = h . s

then s = x by A3, A5, TARSKI:def 1;

hence g . s = h . s by A7; :: thesis: verum

end;assume s in dom g ; :: thesis: g . s = h . s

then s = x by A3, A5, TARSKI:def 1;

hence g . s = h . s by A7; :: thesis: verum